Abstract
A procedure is given for transforming refutation matings into natural deduction proofs. Thus a theorem proving system which establishes the validity of a theorem by the general matings approach can apply this procedure to obtain a comprehensible proof of the theorem without further search. This illuminates the close relationship between matings and proofs, and serves as a step toward a synthesis between apparently quite different approaches to automated theorem proving.
From a refutation mating the system constructs a plan for a theorem, describing appropriate replications of quantifiers, substitutions, and matchings of atoms. Skolem functions play a useful role in refutation matings, but terms involving such functions are replaced by appropriate variables when plans are constructed. Once a plan has been constructed, the system constructs a proof outline, or fragmentary proof, on the basis of the structure of the theorem and general principles for constructing natural deduction proofs. In a proof outline certain lines (planned lines) are justified not by rules of inference, but by plans. The outline is filled in by applying transformation rules, which add additional lines to the proof, justify certain planned lines, and sometimes create new planned lines. The linkage between plans and the proof is maintained by keeping track of the ancestries of wffs and quantifiers in the proof. Using the plans and other information about the proof, the system controls the application of transformation rules. For example, ∀xA(x) is instantiated to A(t) in the proof if the plan requires that t be substituted for a variable corresponding to x. Special problems arise in constructing natural proofs of existentially complex theorems, so they are proved in alternative forms.
This work is supported by National Science Foundation Grant MCS78-01462.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Peter B. Andrews, "Refutations by Matings", IEEE Transactions on Computers C-25 (1976), 801–807.
Peter B. Andrews, "General Matings", Proceedings of the Fourth Workshop on Automated Deduction, Austin, Texas, February 1–3, 1979, 19–25. (Condensation of [3].)
Peter B. Andrews, "Theorem Proving via General Matings", Journal of the ACM (to appear).
W. Bibel, "An Approach to a Systematic Theorem Proving Procedure in First-Order Logic", Computing 12 (1974), 43–55.
W. Bibel and J. Schreiber, "Proof Search in a Gentzen-like System of First Order Logic", Proceedings of the International Computing Symposium 1975, edited by E. Gelenbe and D. Potier, North-Holland Publishing Company, 1975, 205–212.
W. Bibel, "A Syntactic Connection between Proof Procedures and Refutation Procedures", Theoretical Computer Science 3rd GI Conf., Lecture Notes in Computer Science 48, Springer, 1978, 215–224.
Wolfgang Bibel, "A Comparative Study of Several Proof Procedures", Universitat Karlsruhe, (August 1979).
Jacques Herbrand, "Recherches sur la Theorie de la Demonstration", Travaux de la Societe des Sciences et des Lettres de Varsovie, Classe III sciences mathematiques et physiques, no. 33 (1930). Translated in [9].
Jacques Herbrand, Logical Writings, edited by Warren D. Goldfarb, Harvard University Press, 1971, 312pp.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1980 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andrews, P.B. (1980). Transforming matings into natural deduction proofs. In: Bibel, W., Kowalski, R. (eds) 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980. CADE 1980. Lecture Notes in Computer Science, vol 87. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10009-1_22
Download citation
DOI: https://doi.org/10.1007/3-540-10009-1_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-10009-6
Online ISBN: 978-3-540-38140-2
eBook Packages: Springer Book Archive