Advertisement

Logische Grundlagen des maschinellen Beweisens (Resolventenprinzip)

  • Eberhard Bergmann
  • Helga Noll
Chapter
Part of the Heidelberger Taschenbücher book series (HTB, volume 187)

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Zitate aus Kapitel 5

  1. [AL 70]
    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. [AB 70]
    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)MathSciNetzbMATHCrossRefGoogle Scholar
  3. [Bg 73]
    E. Bergmann: Zu den logischen Grundlagen von Beweisprozeduren. Technische Universität Berlin, Fachbereich 20 — Informatik, Bericht Nr. 73–20, 1973Google Scholar
  4. [BN 74]
    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, 1974Google Scholar
  5. [Bi76a]
    W. Bibel: A syntactic connection between proof procedures and refutation procedures. Report, presented at the conference on “Automatic Theorem Proving”, Oberwolfach 1976Google Scholar
  6. [Bi 76b]
    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. [Boy 71]
    R. S. Boyer: Locking: A restriction of resolution. Ph. D. dissertation, Univ. Texas, Austin, 1971Google Scholar
  8. [CL 73]
    C. L. Chang and R. C. T. Lee: Symbolic Logic and Mechanical Theorem Proving. New York, London: Academic Press 1973Google Scholar
  9. [COW 76]
    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. [DP 60]
    M. Davis and H. Putnam: A computing procedure for quantification theory. J.ACM 7, 201–215 (1960)MathSciNetzbMATHGoogle Scholar
  11. [vEK 74]
    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, 1974Google Scholar
  12. [Er 64]
    F. Erwe: Differential- und Integralrechnung I. Mannheim: Bibliogr. Institut 1964Google Scholar
  13. [Gre 69a]
    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. [Gre 69b]
    C. Green: Application of theorem-proving to problem solving. Proc. Intern.Joint Conf. Artificial Intelligence, 219–239 (1969)Google Scholar
  15. [Gil 60]
    P. C. Gilmore: A proof method for quantification theory: its justification and realization. IBM Journal of Research and Development 4, 28–35 (1960)MathSciNetzbMATHCrossRefGoogle Scholar
  16. [Hay 73]
    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. [Hen 75]
    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 1975Google Scholar
  18. Hen 76] L. J. Henschen: Semantic resolution for Horn-sets. IEEE Transaction onGoogle Scholar
  19. [Jac74]
    P. C. Jackson: Introduction to Artificial Intelligence. New York: Petrocelli/ Charter 1974Google Scholar
  20. [Kow70a]
    R. Kowalski: Studies in completeness and efficiency of theorem proving by resolution. Ph. D. Thesis, Univ. of Edinburgh, 1970Google Scholar
  21. [Kow70b]
    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. [Kow 73]
    R. Kowalski: Predicate logic as programming language. Department of Computational Logic, Univ. of Edinburgh, Memo No 70, 1973Google Scholar
  23. Kow 73 a] R. Kowalski: An improved theorem-proving system for first order logic. Meta-Google Scholar
  24. [Kow 74 a]
    R. Kowalski: Logic for problem solving. Department of Computational Logic, Univ. of Edinburgh, Memo No 75, 1974Google Scholar
  25. [Kow 74b]
    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. [KK71]
    R. Kowalski and D. G. Kühner: Linear resolution with selection function. Artificial Intelligence 2, 221–260 (1971)CrossRefGoogle Scholar
  29. [Küh 71]
    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. [Lov 68]
    D. W. Loveland: Mechanical theorem-proving by model elimination. J.ACM 15, 236–251 (1968)MathSciNetzbMATHCrossRefGoogle Scholar
  31. Lov 70] D. W. Loveland: A linear format for resolution. Proc. IRIA Symp. AutomaticGoogle Scholar
  32. Demonstration. Berlin, Heidelberg, New York: Springer 1970, 147–162Google Scholar
  33. LN 71] D. Luckham and N. Nilsson: Extracting information from resolution proofGoogle Scholar
  34. trees. Artificial Intelligence 2, 27–54 (1971)MathSciNetCrossRefGoogle Scholar
  35. [Mas 71]
    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. [Mel 75]
    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–38Google Scholar
  37. [MFM73]
    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)zbMATHCrossRefGoogle Scholar
  38. [Nev 72]
    A. J. Nevins: A human oriented logic for automatic theorem proving. MIT AI Memo No 268, 1972Google Scholar
  39. [Ni 71]
    N. J. Nilsson: Problem Solving Methods in Artificial Intelligence. New York: McGraw-Hill 1971Google Scholar
  40. [No 76]
    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, 1976Google Scholar
  41. [Pra 60]
    D. Prawitz: An improved proof procedure. Theoria 26, 102–139 (1960)MathSciNetzbMATHCrossRefGoogle Scholar
  42. [Ri 75]
    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. [Rob 65]
    J. A. Robinson: A machine-oriented logic based on the resolution principle, J.ACM 12, 23–41 (1965)zbMATHCrossRefGoogle Scholar
  45. [Rob 65a]
    J. A. Robinson: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227–234 (1965)zbMATHGoogle Scholar
  46. [Sa 70]
    H. Sachs: Einführung in die Theorie der endlichen Graphen. Leipzig: Teubner 1970zbMATHGoogle Scholar
  47. [Sla 67]
    J. R. Slagle: Automatic theorem proving with renamable and semantic resolution. J.ACM 14, 687–697 (1967)MathSciNetzbMATHCrossRefGoogle Scholar
  48. [Sla 71]
    J. R. Slagle: Artificial Intelligence: The Heuristic Programming Approach. New York: McGraw-Hill 1971Google Scholar
  49. [SCL 69]
    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. [Sti 73]
    R. B. Stillman: The concept of weak substitution in theorem proving. J.ACM 20, 648–667 (1973)MathSciNetzbMATHCrossRefGoogle Scholar
  51. [THEO 74]
    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, 1974Google Scholar
  52. [Vee 71]
    G. Veenker: Maschinelles Beweisen. Angewandte Informatik 6, 277–282 (1971)Google Scholar
  53. [WM 76]
    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. [WCR 64]
    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. [WCR 65]
    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)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1977

Authors and Affiliations

  • Eberhard Bergmann
    • 1
  • Helga Noll
    • 1
  1. 1.Fachbereich Informatik Informatik-Forschungsgruppen Programmiersprachen und Compiler I Computergestützte InformationssystemeTechnische Universität BerlinGermany

Personalised recommendations