Zusammenfassung
Ausgehend von einer speziellen Formulierung des Prädikatenkalküls 1. Stufe werden zwei Verfahren entwickelt, welche Widerlegungen inkonsistenter FormelnF liefern. Grundlegend für beide Verfahren ist der Begriff der Verkettung von Literals. Das erste beruht auf demHerbrad-Theorem. SeiF ndie Konjunktion vonn Exemplaren der FormelF. Es wird ein Algorithmus angegeben, der entscheidet, ob es bei gegebenemn eine Belegung β der Variablen vonF ngibt, bei welcher die Formel βF nvollständig verkettet ist. Die Anwendung dieses Algorithmus fürn=1,2, ... führt zur Konstruktion einer aussagenlogisch inkonsistenten Formel minimaler Länge. Das zweite Verfahren beruht darauf, daß neue Clausen erzeugt werden, die aus nur einem Literal bestehen (und die mitF konsistent sind). Dieses Verfahren ist nicht vollständig, liefert aber in vielen Fällen schnellere Widerlegungen als andere Methoden; einige Maschinen-Protokolle solcher Widerlegungen sind im Anhang zusammengestellt. Das Verfahren läßt sich verallgemeinern; insbesondere bietet es eine Möglichkeit des Zusammenwirkens von Mensch und Maschine beim Beweisen mathematischer Sätze.
Summary
Starting from a special formulation of first order functional calculus two procedures are presented producing refutations of inconsistent formulas. Both procedures are based on the notion of interconnecting literals. The first one goes back toHerbrand's Theorem. LetF nbe the conjunction ofn copies of the formulaF. An algorithm is introduced to decide whether, for a fixedn, there is an assignment β for the variables ofF nmaking the formula βF ncompletely interconnected. By applying this algorithm forn=1,2,... a truth-functionally inconsistent formula of minimal length is constructed. The basic idea of the second procedure is to produce fromF new oneliteral clauses (which are consisten withF). In many cases this proofprocedure, while not complete, is very effective in comparison with other programs; some examples of machine-refutations are given in the appendix. The method may be generalized; in particular it suggests a possibility of man-machine interaction in theorem-proving.
Literatur
Church, A.: Introduction to Mathematical Logic. Vol. I., Princeton. 1956.
Cooper, D. C.: Theorem proving in computers. Advances in Programming and Nonnumerical Computation (L. Fox, Ed.), 155–182. Oxford. 1966.
Darlington, J. L.: Some theorem-proving strategies based on the resolution principle (Manuskript). Bonn. 1966.
Davis, M.: Eliminating the irrelevant from mechanical proofs. Experimental Arithmetic, High Speed Computing and Mathematics (Proc. Symp. Appl. Math., Vol. XV), 15–30. A. M. S. 1963.
Davis, M. andH. Putnam: A computing method for quantification theory. Journ. A. C. M.7, 201–215 (1960).
Davis, M., G. Logemann andD. Loveland: A machine program for theoremproving. Comm. A. C. M.5, 394–397 (1962).
Dunham, B., R. Fridshal andG. L. Sward: A non-heuristic program for proving elementary logical theorems. Proc. I. C. I. P., 282–285. Paris. 1959.
Dunham, B. andJ. H. North: Theorem testing by computer. Proc. Symp. Mathematical Theory of Automata, 173–177. New York. 1963.
Gilmore, P. C.: A proof method for quantification theory: its justification and realisation. IBM-Journ. Res. Dev.4, 28–35 (1960).
Hilbert, D. undW. Ackermann: Grundzüge der theoretischen Logik. 4. Aufl. Berlin-Göttingen-Heidelberg: Springer. 1959.
Hintikka, K. J. J.: Vicious circle principle and the paradoxes. Journ. Symb. Logic22, 245–249 (1957).
Meltzer, B.: Theorem-proving for computers: some results on resolution and renaming. Computer Journ.8, 341–343 (1965/66).
Prawitz, D.: An improved proof procedure. Theoria26, 102–139 (1960).
Quine, W. V. O.: A proof procedure for quantification theory. Journ. Symb. Logic20, 141–149 (1955).
Robinson, J. A.: Theorem proving on the computer. Journ. A. C. M.10, 163–174 (1963).
Robinson, J. A.: A machine-oriented logic based on the resolution principle. Journ. A. C. M.12, 23–41 (1965).
Robinson, J. A.: Automatic deduction with hyper-resolution. Intern. Journ. of Computer Math.1, 227–234 (1965).
Veenker, G.: Ein Entscheidungsverfahren für den Aussagenkalkül und seine Realisation in einem Rechenautomaten. Grundlagstud. Kyb. Geisteswiss.4, 127–136 (1963).
Veenker, G.: Beweisverfahren für den Prädikatenkalkül. Dissertation, Tübingen. 1967.
Wang, H.: Towards mechanical mathematics. IBM-Journ. Res. Dev.4, 2–22 (1960).
Wang, H.: Proving theorems by pattern recognition, I. Comm. A. C. M.3, 220–234 (1960); II. Bell System Techn. Journ.40, 1–41 (1961).
Wang, H.: Formalisation and automatic theorem-proving. Proc. I. F. I. P., Part I, 51–58. New York 1965.
Wos, L., D. Carson andG. Robinson: The unit preference strategy in theorem proving. Proc. A. F. I. P. S.26, 615–621 (1964).
Wos, L., D. Carson andG. Robinson: Efficiency and completeness of the set of support strategy in theorem proving. Journ. A. C. M.12, 536–541 (1965).
Author information
Authors and Affiliations
Additional information
Mit 1 Textabbildung
Dieser Beitrag ist ein Auszug aus der Dissertation [19] des Verfassers.
Rights and permissions
About this article
Cite this article
Veenker, G. Beweisalgorithmen für die Prädikatenlogik. Computing 2, 263–283 (1967). https://doi.org/10.1007/BF02236612
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02236612