Constructive matching — Explanation based methodology for inductive theorem proving
Given formula F and axioms, theorem proving methods try to prove F. If F is provable, the proof obtained provides an explanation of the fact that F is a theorem. It may happen that F is FALSE or, for some reason, that we fail to prove F. Several theorem proving methods provide different kinds of the so-called "failure formulae". The failure formulae explain why the proof of F failed.
This paper illustrates the kind of failure formulae generated by the methodology we have developed for inductive theorem proving of theorems containing existential quantifiers. We reveal the importance of the failure formula vocabulary for generating of the so called missing lemmas.
The paper uses the vocabulary presented in .
KeywordsInduction Hypothesis Theorem Prove Atomic Formula Existential Quantifier Partial Program
Unable to display preview. Download preview PDF.
- W. Bibel, K. M. Hoernig: LOPS — A System Based on a Strategical Approach to Program Synthesis; in , 69–91.Google Scholar
- A. Biermann, G. Guiho, Y. Kodratoff (ed): Automatic Program Construction Techniques; Macmillan Publishing Company, London, 1984.Google Scholar
- S. Biundo: A synthesis system mechanizing proofs by induction; in: ECAI' 86 Proceedings, Vol. 1, 1986, 69–78.Google Scholar
- R. S. Boyer, J S. Moore: A Computational Logic; Academic Press, 1979.Google Scholar
- N. Dershowitz: Synthesis by Completion; in , 208–214.Google Scholar
- M. Franova: Fundamentals for a new methodology for inductive theorem proving: CM-construction of atomic formulae; in , 137–141.Google Scholar
- M. Franova: Fundamentals of a new methodology for Program Synthesis from Formal Specifications: CM-construction of atomic formulae; Thesis, Université Paris-Sud, November, Orsay, France, 1988.Google Scholar
- M. Franova: Precomas 0.3 User Guide; Rapport de Recherche No.524, L.R.I., Université de Paris-Sud, Orsay, France, October, 1989.Google Scholar
- A. K. Joshi, (ed): Proceedings of the Ninth International Joint Conference on Artificial Intelligence; August, Los Angeles, 1985.Google Scholar
- Y. Kodratoff, M.Picard: Complétion de systèmes de réécriture et synthèse de programmes à partir de leurs spécifications; Bigre No.35, October, 1983.Google Scholar
- Y. Kodratoff: An Introduction to Machine Learning; Pitman, London, 1988.Google Scholar
- Y. Kodratoff: Proceedings of the 8th European Conference on Artificial Intelligence; August 1–5, Pitman, London, United Kingdom, 1988.Google Scholar
- R. Michalski, J. G. Carbonell, T. M. Mitchell (eds): Machine Learning: An Artificial Intelligence Approach; Tioga, Palo Alto, California, 1983.Google Scholar
- T. M. Mitchell: Learning by experimentation, acquiring and refining problem-solving heuristics; in , 163–190.Google Scholar
- H. Perdrix: Program synthesis from specifications; ESPRIT'85, Status Report of Continuing Work, North-Holland, 1986, 371–385.Google Scholar
- M. Franova: Explanations in inductive theorem proving; to appear in Proceedings of the AAAI 90 Workshop on Learning.Google Scholar
- G. DeJong, R. Mooney: Explanation-Based Learning: An Alternative View; Machine Learning 1, 1986, 145–176.Google Scholar
- K. L. Clark, J. Darlington: Algorithm classification through synthesis; The Computer Journal, Vol. 23, No 1, 61–65.Google Scholar