Abstract
A complexity degree for theorems in first-order logic is introduced which naturally reflects the difficulty of proving them. Relative to that degree it is required that a systematic proof procedure should prove simple theorems faster than harder ones. Such a systematic but relatively inefficient procedure and a semisystematic but efficient procedure are presented. Both are developed on the basis of the consistency and completeness theorem for the underlying formal system rather than Herbrand's theorem.
Zusammenfassung
Für Theoreme der Prädikatenlogik erster Stufe wird ein Komplexitätsgrad eingeführt, der in natürlicher Weise die Kompliziertheit der zugehörigen Beweise mißt. Im Sinne dieses Grades wird von einer systematischen Beweisprozedur verlangt, daß sie einfache Theoreme schneller beweist als schwierigere. Solch ein systematisches, jedoch relativ ineffizientes Verfahren und ein halb-systematisches, jedoch effizientes Verfahren werden in dieser Arbeit beschrieben. Beide Verfahren stützen sich auf den Konsistenz- und Vollständigkeitssatz des zugrundeliegenden formalen Systems und nicht, wie üblich, auf den Herbrand-Satz.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Bibel, W.: Schnittelimination in einem Teilsystem der einfachen Typenlogik. Archiv f. Math. Logik12, 159–178 (1969).
Ernst, G. W.: The utility of independent subgoals in theorem proving. Inform. and Contr.18, 237–252 (1971).
Prawitz, D.: An improved proof procedure. Theoria26, 102–139 (1960).
Prawitz, D.: A proof procedure with matrix reduction. In: Symposium on Atomic Demonstration, 1968. (Lect. notes in Mathem., vol. 125.) Berlin-Heidelberg-New York: Springer. 1970.
Robinson, J. A.: A review of automatic theorem-proving. Proc. Symp. Appl. Math., Amer. Math. Soc.19, 1966.
Schütte, K.: Beweistheorie. Berlin: 1960.
Wang, H.: Toward mechanical mathematics. IBM Journal1960, 2–22.
Nilsson, N. J.: Problem-solving methods in artificial intelligence. New York: 1971.
Author information
Authors and Affiliations
Additional information
With 1 Figure
Rights and permissions
About this article
Cite this article
Bibel, W. An approach to a systematic theorem proving procedure in first-order logic. Computing 12, 43–55 (1974). https://doi.org/10.1007/BF02239498
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02239498