Skip to main content
SpringerLink
Log in
Book cover

Mathematische Logik mit Informatik-Anwendungen pp 155–237Cite as

Logische Grundlagen des maschinellen Beweisens (Resolventenprinzip)

  • Chapter

  • 91 Accesses

Part of the book series: Heidelberger Taschenbücher ((HTB,volume 187))

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   69.95
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Zitate aus Kapitel 5

  1. J. Allen and D. Luckham: An interactive theorem-proving program. Machine Intelligence, B. Meitzer and D. Michie (Ed.), New York: American-Elsevier, Vol 4, 321–336 (1970)

    Google Scholar 

  2. R. Anderson and W. W. Bledsoe: A linear format for resolution with merging and a new technique for establishing completeness. J.ACM 17, 525–534 (1970)

    Article  MathSciNet  MATH  Google Scholar 

  3. E. Bergmann: Zu den logischen Grundlagen von Beweisprozeduren. Technische Universität Berlin, Fachbereich 20 — Informatik, Bericht Nr. 73–20, 1973

    Google Scholar 

  4. E. Bergmann und H. Noll: Horn-Formeln, eine durch Anwendung motivierte Einschränkung von Eingaben für Theorem-Beweiser. Technische Universität Berlin, Fachbereich 20 — Informatik, Bericht Nr. 74–30, 1974

    Google Scholar 

  5. W. Bibel: A syntactic connection between proof procedures and refutation procedures. Report, presented at the conference on “Automatic Theorem Proving”, Oberwolfach 1976

    Google Scholar 

  6. W. Bibel: Maschinelles Beweisen. In: Jahrbuch Überblicke Mathematik 1976. B. Fuchssteiner, U. Kulisch, D. Laugwitz, R. Liedl (Hrsg.). Mannheim, Wien, Zürich: Bibliogr. Institut, 115–142 (1976)

    Google Scholar 

  7. R. S. Boyer: Locking: A restriction of resolution. Ph. D. dissertation, Univ. Texas, Austin, 1971

    Google Scholar 

  8. C. L. Chang and R. C. T. Lee: Symbolic Logic and Mechanical Theorem Proving. New York, London: Academic Press 1973

    Google Scholar 

  9. J. D. McCharen, R. A. Overbeek and L. A. Wos: Problems and experiments for and with automated theorem-proving programs. IEEE Transaction on Computers, Vol C-25, no 8, 773–782 (1976)

    Google Scholar 

  10. M. Davis and H. Putnam: A computing procedure for quantification theory. J.ACM 7, 201–215 (1960)

    MathSciNet  MATH  Google Scholar 

  11. M. H. van Emden and R. Kowalski: The semantics of predicate logic as a programming language. Department of Computational Logic, Univ. of Edinburgh, Memo No 73, 1974

    Google Scholar 

  12. F. Erwe: Differential- und Integralrechnung I. Mannheim: Bibliogr. Institut 1964

    Google Scholar 

  13. C. Green: Theorem-proving by resolution as a basis for question-answering systems, Machine Intelligence, B. Meitzer and D. Michie (Ed.), New York: American-Elsevier, Vol 4, 183–205 (1969)

    Google Scholar 

  14. C. Green: Application of theorem-proving to problem solving. Proc. Intern.Joint Conf. Artificial Intelligence, 219–239 (1969)

    Google Scholar 

  15. P. C. Gilmore: A proof method for quantification theory: its justification and realization. IBM Journal of Research and Development 4, 28–35 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  16. P. J. Hayes: Computation and deduction. Proc. of the Symposion on Mathematical Foundations of Computer Science, Czechoslovakian Academy of Sciences, 105–117 (1973)

    Google Scholar 

  17. L. J. Henschen: Principles of the construction of programming languages for the experimentation with theorem-provers. Northwestern Univ., Evanston, Illinois. Report, vorgetragen an der Technischen Universität Berlin 1975

    Google Scholar 

  18. Hen 76] L. J. Henschen: Semantic resolution for Horn-sets. IEEE Transaction on

    Google Scholar 

  19. P. C. Jackson: Introduction to Artificial Intelligence. New York: Petrocelli/ Charter 1974

    Google Scholar 

  20. R. Kowalski: Studies in completeness and efficiency of theorem proving by resolution. Ph. D. Thesis, Univ. of Edinburgh, 1970

    Google Scholar 

  21. R. Kowalski: Search strategies for theorem-proving. Machine Intelligence, B. Meitzer and D. Michie (Ed.), New York: American-Elsevier, Vol 5,181–201 (1970)

    Google Scholar 

  22. R. Kowalski: Predicate logic as programming language. Department of Computational Logic, Univ. of Edinburgh, Memo No 70, 1973

    Google Scholar 

  23. Kow 73 a] R. Kowalski: An improved theorem-proving system for first order logic. Meta-

    Google Scholar 

  24. R. Kowalski: Logic for problem solving. Department of Computational Logic, Univ. of Edinburgh, Memo No 75, 1974

    Google Scholar 

  25. R. Kowalski: Predicate Logic as programming language. Proc. of the IFIP-Congress, Stockholm, 569–574 (1974)

    Google Scholar 

  26. R. Kowalski and P. J. Hayes: Semantic trees in automatic theorem-proving.

    Google Scholar 

  27. Machine Intelligence, B. Meitzer and D. Michie (Ed.), New York: American-Elsevier, Vol 4, 87–101 (1969)

    Google Scholar 

  28. R. Kowalski and D. G. Kühner: Linear resolution with selection function. Artificial Intelligence 2, 221–260 (1971)

    Article  Google Scholar 

  29. D. G. Kühner: A note on the relation between resolution and Maslov’s inverse method. Machine Intelligence, B. Meltzer and D. Michie (Ed.), New York: American-Elsevier, Vol 6, 73–90 (1971)

    Google Scholar 

  30. D. W. Loveland: Mechanical theorem-proving by model elimination. J.ACM 15, 236–251 (1968)

    Article  MathSciNet  MATH  Google Scholar 

  31. Lov 70] D. W. Loveland: A linear format for resolution. Proc. IRIA Symp. Automatic

    Google Scholar 

  32. Demonstration. Berlin, Heidelberg, New York: Springer 1970, 147–162

    Google Scholar 

  33. LN 71] D. Luckham and N. Nilsson: Extracting information from resolution proof

    Google Scholar 

  34. trees. Artificial Intelligence 2, 27–54 (1971)

    Article  MathSciNet  Google Scholar 

  35. S. J. Maslov: Proof search strategies for methods of the resolution type. Machine Intelligence, B. Meitzer and D. Michie (Ed.), New York: American- Elsevier, Vol 6, 77–90 (1971)

    Google Scholar 

  36. B. Meitzer: Vorbemerkungen zu einer Theorie der Effizienz von Beweisver¬fahren. Künstliche Intelligenz und Heuristisches Programmieren. Erweiterte Bearbeitung der englischen Ausgabe, Herausgeber N. V. Findler, übersetzt von O. Itzinger, New York: Springer 1975, 15–38

    Google Scholar 

  37. J. Minker, D.H. Fishman and J.R. McSkimin: The (Q*-algorithm—a search strategy for a deductive question-answering system. Artificial Intelligence 4, 225–243 (1973)

    Article  MATH  Google Scholar 

  38. A. J. Nevins: A human oriented logic for automatic theorem proving. MIT AI Memo No 268, 1972

    Google Scholar 

  39. N. J. Nilsson: Problem Solving Methods in Artificial Intelligence. New York: McGraw-Hill 1971

    Google Scholar 

  40. H. Noll: Eine konstruktive Formulierung des Lifting-Theorems unter expliziter Angabe der liftenden Substitutionen und eine Anwendung auf Faktori-sierungs-Einschränkungen. Dissertation, Technische Universität Berlin, Fachbereich 20 — Informatik, 1976

    Google Scholar 

  41. D. Prawitz: An improved proof procedure. Theoria 26, 102–139 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  42. M. M. Richter: Resolution, paramodulation and Gentzen-systems. Schriften zur Informatik und Angewandten Mathematik, RWTH Aachen, Bericht Nr. 23 (1975)

    Google Scholar 

  43. Rob 63] J. A. Robinson: Theorem proving on the computer. J.ACM 10,163–174(1963)

    Google Scholar 

  44. J. A. Robinson: A machine-oriented logic based on the resolution principle, J.ACM 12, 23–41 (1965)

    Article  MATH  Google Scholar 

  45. J. A. Robinson: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227–234 (1965)

    MATH  Google Scholar 

  46. H. Sachs: Einführung in die Theorie der endlichen Graphen. Leipzig: Teubner 1970

    MATH  Google Scholar 

  47. J. R. Slagle: Automatic theorem proving with renamable and semantic resolution. J.ACM 14, 687–697 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  48. J. R. Slagle: Artificial Intelligence: The Heuristic Programming Approach. New York: McGraw-Hill 1971

    Google Scholar 

  49. J. R. Slagle, C. L. Chang and R. C. T. Lee: Completeness theorems for semantic resolution in consequence finding. Proc. Intern. Joint Conf. Artif. Intelligence, 281–285 (1969)

    Google Scholar 

  50. R. B. Stillman: The concept of weak substitution in theorem proving. J.ACM 20, 648–667 (1973)

    Article  MathSciNet  MATH  Google Scholar 

  51. Beweisprogramm aus „G. Kook and J. van Vaalen: An automatic theorem- prover. Mathematisch Centrum Amsterdam, Bericht Nr. 22, 1971”, modifiziert und installiert an der Technischen Universität Berlin, Fachbereich 20 — Informatik, 1974

    Google Scholar 

  52. G. Veenker: Maschinelles Beweisen. Angewandte Informatik 6, 277–282 (1971)

    Google Scholar 

  53. G. A. Wilson and J. Minker: Resolution, refinements and search strategies: a comparative study. IEEE Transactions on Computers, Vol C-25, no 8, 782–800 (1976)

    Google Scholar 

  54. L. T. Wos, D. F. Carson and G. A. Robinson: The unit preference strategy in theorem proving. Proc. AFIPS Fall Joint Comput. Conf. 26, 616–621 (1964)

    Google Scholar 

  55. L. T. Wos, D. F. Carson and G. A. Robinson: Efficiency and completeness of the set of support strategy in theorem proving. J.ACM 12, 536–541 (1965)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik Informatik-Forschungsgruppen Programmiersprachen und Compiler I Computergestützte Informationssysteme, Technische Universität Berlin, Germany

    Eberhard Bergmann & Helga Noll

Authors
  1. Eberhard Bergmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Helga Noll
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1977 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Bergmann, E., Noll, H. (1977). Logische Grundlagen des maschinellen Beweisens (Resolventenprinzip). In: Mathematische Logik mit Informatik-Anwendungen. Heidelberger Taschenbücher, vol 187. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-66635-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-66635-3_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-08202-6

  • Online ISBN: 978-3-642-66635-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation