Advertisement

Logische Grundlagen des maschinellen Beweisens (Resolventenprinzip)

  • Eberhard Bergmann
  • Helga Noll
Chapter
  • 66 Downloads
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