Abstract
Theorem proving is difficult and deals with complex phenomena. The difficulties seem to be compounded when one works with higher-order logic, but the rich expressive power of Church's formulation [10] [3] of this language makes research on theorem proving in this realm very worthwhile. In order to make significant progress on this problem, we need to try many approaches and ideas, and explore many questions. A highly relevant question is "What makes a logical formula valid?".
One approach to this question is semantic. Theorems are true because they express essential truths and thus are true in all models of the language in which they are expressed. Truth can be perceived from many perspectives, so there may be many essentially different proofs of theorems. This point of view is very appealing, but it does not shed much light on the basic question of what makes certain sentences true in all models, while others are not.
Of course, theorems are formulas which have proofs, and every proof in any logical system may provide some insight. This suggests seeing what one can learn by studying the forms proofs can take. While this may be helpful, many of the most prominent features of proofs seem to be influenced as much by the logical system in which the proof is given as by the theorem that is being proved.
We focus on trying to understand what there is about the syntactic structures of theorems that makes them valid. In the case of formulas of propositional calculus, one can test a formula for being a tautology in an explicit syntactic way. However, simply checking each line of a truth table is not really very enlightening, and we may still find ourselves asking "What is there about the structure of this formula which makes it a tautology?". Clearly the pattern of occurrences of positive and negative literals in such a formula is very important, and this leads to the theory of connections or matings [4] [1] [6]. A connection is a pair of literal-occurrences, and a mating is a set of connections, i.e., a relation between occurrences of literals. A mating is acceptable if its structure guarantees that the formula is a tautology. Perhaps much more can be said about criteria for matings to be acceptable.
This work is supported by NSF grant DCR-8402532.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Peter B. Andrews, Theorem Proving via General Matings, Journal of the ACM 28 (1981), 193–214.
Peter B. Andrews, Dale A. Miller, Eve Longini Cohen, Frank Pfenning, "Automating Higher-Order Logic," in Automated Theorem Proving: After 25 Years, edited by W. W. Bledsoe and D. W. Loveland, Contemporary Mathematics series, vol. 29, American Mathematical Society, 1984, 169–192.
Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press, 1986.
Wolfgang Bibel, On Matrices with Connections, Journal of the ACM 28 (1981), 633–645.
Wolfgang Bibel, Automated Theorem Proving, Vieweg, Braunschweig, 1982.
Wolfgang Bibel, Matings in Matrices, Communications of the ACM 26 (1983), 844–852.
Wolfgang Bibel and Bruno Buchberger, Towards a Connection Machine for Logical Inference, Future Generations Computer Systems 1 (1984–1985).
W. W. Bledsoe, "A Maximal Method for Set Variables in Automatic Theorem Proving," in Machine Intelligence 9, Ellis Harwood Ltd., Chichester, 1979, pp. 53–100.
W. W. Bledsoe. Using Examples to Generate Instantiations for Set Variables, ATP-67, University of Texas at Austin, July 1982, 44 pp
Alonzo Church, A Formulation of the Simple Theory of Types, Journal of Symbolic Logic 5 (1940), 56–68.
Gérard P. Huet, "A Mechanization of Type Theory," in Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI, 1973, 139–146.
Gérard P. Huet, A Unification Algorithm for Typed λ-Calculus, Theoretical Computer Science 1 (1975), 27–57.
D. C. Jensen and T. Pietrzykowski, Mechanizing ω-Order Type Theory Through Unification, Theoretical Computer Science 3 (1976), 123–171.
Dale A. Miller. Proofs in Higher-Order Logic, Ph.D. Thesis, Carnegie-Mellon University, October, 1983. 81 pp.
Dale A. Miller, "Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs," in 7th International Conference on Automated Deduction, Napa, California, USA, edited by R. E. Shostak, Lecture Notes in Computer Science 170, Springer-Verlag, May 14–16, 1984, 375–393.
Frank Pfenning, "Analytic and Non-analytic Proofs," in 7th International Conference on Automated Deduction, Napa, California, USA, edited by R. E. Shostak, Lecture Notes in Computer Science 170, Springer-Verlag, May 14–16, 1984, 394–413.
Frank Pfenning. Proof Transformations in Higher-Order Logic, Ph.D. Thesis, Carnegie-Mellon University, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andrews, P.B. (1986). Connections and higher-order logic. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_75
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_75
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive