Aformal approach to some usually informal techniques used in mathematical reasoning
One of the striking characteristics of mathematical reasoning is the contrast between the formal aspects of mathematical truth and the informal character of the ways to that truth. Among the many important and usually informal mathematical activities we are interested by proof analogy (i.e. common pattern between proofs of different theorems) in the context of interactive theorem proving. In some sense we propose a partial contribution of one of the Polya's wishes [Polya 73]:
"Analogy pervades all our thinking, our everyday speech and our trivial conclusions as well as artistic way of expression and the highest scientific achievements...but analogy may reach the level of mathematical precision..."
It is a work in philosophy of mathematics [Resnik 75], in which mathematics is viewed as studying patterns or structures, which encouraged us to pursue our aim of partially formalizing analogy. We naturally arrived at the need of considering other activities strongly tied to the notion of analogy and very well known of the working mathematician: generalization, abstraction and analysis of proofs.
We propose a method to deal with proof analogy in interactive theorem proving where the paradigm of "proposition as types" is adopted, proofs are represented as terms and a higher-order language L is available to the user.
Let us assume that the user has to prove a conjecture C. Given a proof P for a known theorem T, he describes in the language L a scheme of P. Then he expresses the syntactic analogy he views as relevant between the scheme of P and what "should be" a proof scheme for C, as a transformation rule. This process needs analysis of proofs, generalization and abstraction.
A second order pattern matching algorithm constructs matchers of P and its scheme, and applies them to the intended proof scheme of the conjecture C. In the best case one obtains a potential proof of C, but in general one obtains a more instantiated proof-scheme with some "holes" to be filled by a theorem prover. In both cases a proof-checking process is necessary (analogy is in general a heuristic way of thinking).
The given proof P and its proposed scheme are not matchable.
A type error is detected in the instantiated proof scheme for C.
We give in the following a method to suggest lemmas in the first case, and sketch some ideas of how to use such a possibility in the second case.
Unable to display preview. Download preview PDF.
- [Boy de la Tour 87]T. Boy de la Tour, R. Caferra: "Proof analogy in interactive theorem proving: a method to express and use it via second order pattern matching"; Proc. of the AAAI-87; Seattle, U.S.A., July 1987, 95–99.Google Scholar
- [Bundy 85]A. Bundy: "Discovery and reasoning in Mathematics"; Proc. of the 9th. IJCAI. Los Angeles, U.S.A., August 1985, 1221–1230.Google Scholar
- [Constable 85]R. L. Constable, T. B. Knoblock, J. L. Bates: "Writing programs that construct proofs";Journal of Automated Reasoning 1, 1985, 285–326.Google Scholar
- [Gelernter 63]H. Gelernter, J. R. Hansen, D. W. Loveland: "Empirical explorations of the geometry-theorem proving machine"; in "Computers and Thought" (E. Feigenbaum and J. Feldman eds.), McGraw-Hill, 1963, 153–163.Google Scholar
- [Huet 78]G. Huet, B. Lang: "Proving and applying program transformations expressed with second-order patterns"; Acta Informatica 11, 1978, 31–55.Google Scholar
- [Huet 86]G. Huet: "Formal structures for computation and deduction". First edition, May 1986.Google Scholar
- [Kling 71]R. E. Kling: "A paradigm for reasoning by analogy"; Artificial Intelligence 2, 1971, 147–178.Google Scholar
- [Leivant 83]D. Leivant: "Polymorphic Type Inference", Proc. 10th. ACM Symp. On Principles of Programming Languages, 1983, 88–98.Google Scholar
- [Loveland 78]D.W. Loveland: "Automated theorem proving: a logical basis". North-Holland 1978.Google Scholar
- [Milner 78]R. Milner: "A Theory of Type Polymorphism in Programming"; Journal of Computer and System Sciences 17 (1978), 348–375.Google Scholar
- [Milner 85]R. Milner: "The use of machines to assist in rigorous proof" in "Mathematical Logic and Programming Languages" (C.A.R. Hoare and J.C. Shepherdson, eds.), Prentice-Hall 1985, pp.77–88.Google Scholar
- [Pfenning 84]F. Pfenning: "Analytic and Non-analytic Proofs"; Proc. 7th. International Conference on Automated Deduction, California, USA. Lecture Notes in Computer Science 170, Springer-Verlag 1984, 394–413.Google Scholar
- [Plaisted 81]D. A. Plaisted: "Theorem proving with abstraction"; Artificial Intelligence 16, 1981, 47–108.Google Scholar
- [Polya 73]G. Polya: "How to solve it, a new aspect of mathematical method". Princeton University Press, 2nd. ed., 1973.Google Scholar
- [Resnik 75]M.D. Resnik: "Mathematical knowledge and pattern cognition"; Canadian Journal of Philosophy, volume 5, Number 1, September 1975, pp. 25–39.Google Scholar