Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Zitate aus Kapitel 5
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)
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)
E. Bergmann: Zu den logischen Grundlagen von Beweisprozeduren. Technische Universität Berlin, Fachbereich 20 — Informatik, Bericht Nr. 73–20, 1973
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
W. Bibel: A syntactic connection between proof procedures and refutation procedures. Report, presented at the conference on “Automatic Theorem Proving”, Oberwolfach 1976
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)
R. S. Boyer: Locking: A restriction of resolution. Ph. D. dissertation, Univ. Texas, Austin, 1971
C. L. Chang and R. C. T. Lee: Symbolic Logic and Mechanical Theorem Proving. New York, London: Academic Press 1973
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)
M. Davis and H. Putnam: A computing procedure for quantification theory. J.ACM 7, 201–215 (1960)
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
F. Erwe: Differential- und Integralrechnung I. Mannheim: Bibliogr. Institut 1964
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)
C. Green: Application of theorem-proving to problem solving. Proc. Intern.Joint Conf. Artificial Intelligence, 219–239 (1969)
P. C. Gilmore: A proof method for quantification theory: its justification and realization. IBM Journal of Research and Development 4, 28–35 (1960)
P. J. Hayes: Computation and deduction. Proc. of the Symposion on Mathematical Foundations of Computer Science, Czechoslovakian Academy of Sciences, 105–117 (1973)
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
Hen 76] L. J. Henschen: Semantic resolution for Horn-sets. IEEE Transaction on
P. C. Jackson: Introduction to Artificial Intelligence. New York: Petrocelli/ Charter 1974
R. Kowalski: Studies in completeness and efficiency of theorem proving by resolution. Ph. D. Thesis, Univ. of Edinburgh, 1970
R. Kowalski: Search strategies for theorem-proving. Machine Intelligence, B. Meitzer and D. Michie (Ed.), New York: American-Elsevier, Vol 5,181–201 (1970)
R. Kowalski: Predicate logic as programming language. Department of Computational Logic, Univ. of Edinburgh, Memo No 70, 1973
Kow 73 a] R. Kowalski: An improved theorem-proving system for first order logic. Meta-
R. Kowalski: Logic for problem solving. Department of Computational Logic, Univ. of Edinburgh, Memo No 75, 1974
R. Kowalski: Predicate Logic as programming language. Proc. of the IFIP-Congress, Stockholm, 569–574 (1974)
R. Kowalski and P. J. Hayes: Semantic trees in automatic theorem-proving.
Machine Intelligence, B. Meitzer and D. Michie (Ed.), New York: American-Elsevier, Vol 4, 87–101 (1969)
R. Kowalski and D. G. Kühner: Linear resolution with selection function. Artificial Intelligence 2, 221–260 (1971)
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)
D. W. Loveland: Mechanical theorem-proving by model elimination. J.ACM 15, 236–251 (1968)
Lov 70] D. W. Loveland: A linear format for resolution. Proc. IRIA Symp. Automatic
Demonstration. Berlin, Heidelberg, New York: Springer 1970, 147–162
LN 71] D. Luckham and N. Nilsson: Extracting information from resolution proof
trees. Artificial Intelligence 2, 27–54 (1971)
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)
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
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)
A. J. Nevins: A human oriented logic for automatic theorem proving. MIT AI Memo No 268, 1972
N. J. Nilsson: Problem Solving Methods in Artificial Intelligence. New York: McGraw-Hill 1971
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
D. Prawitz: An improved proof procedure. Theoria 26, 102–139 (1960)
M. M. Richter: Resolution, paramodulation and Gentzen-systems. Schriften zur Informatik und Angewandten Mathematik, RWTH Aachen, Bericht Nr. 23 (1975)
Rob 63] J. A. Robinson: Theorem proving on the computer. J.ACM 10,163–174(1963)
J. A. Robinson: A machine-oriented logic based on the resolution principle, J.ACM 12, 23–41 (1965)
J. A. Robinson: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227–234 (1965)
H. Sachs: Einführung in die Theorie der endlichen Graphen. Leipzig: Teubner 1970
J. R. Slagle: Automatic theorem proving with renamable and semantic resolution. J.ACM 14, 687–697 (1967)
J. R. Slagle: Artificial Intelligence: The Heuristic Programming Approach. New York: McGraw-Hill 1971
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)
R. B. Stillman: The concept of weak substitution in theorem proving. J.ACM 20, 648–667 (1973)
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
G. Veenker: Maschinelles Beweisen. Angewandte Informatik 6, 277–282 (1971)
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)
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)
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)
Author information
Authors and Affiliations
Rights 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