Constructive matching — Explanation based methodology for inductive theorem proving

  • Marta Fraňová
Part III Communications
Part of the Lecture Notes in Computer Science book series (LNCS, volume 464)


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 [7].


Induction Hypothesis Theorem Prove Atomic Formula Existential Quantifier Partial Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    W. Bibel, K. M. Hoernig: LOPS — A System Based on a Strategical Approach to Program Synthesis; in [2], 69–91.Google Scholar
  2. [2]
    A. Biermann, G. Guiho, Y. Kodratoff (ed): Automatic Program Construction Techniques; Macmillan Publishing Company, London, 1984.Google Scholar
  3. [3]
    S. Biundo: A synthesis system mechanizing proofs by induction; in: ECAI' 86 Proceedings, Vol. 1, 1986, 69–78.Google Scholar
  4. [4]
    R. S. Boyer, J S. Moore: A Computational Logic; Academic Press, 1979.Google Scholar
  5. [5]
    N. Dershowitz: Synthesis by Completion; in [9], 208–214.Google Scholar
  6. [6]
    M. Franova: Fundamentals for a new methodology for inductive theorem proving: CM-construction of atomic formulae; in [12], 137–141.Google Scholar
  7. [7]
    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
  8. [8]
    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
  9. [9]
    A. K. Joshi, (ed): Proceedings of the Ninth International Joint Conference on Artificial Intelligence; August, Los Angeles, 1985.Google Scholar
  10. [10]
    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
  11. [11]
    Y. Kodratoff: An Introduction to Machine Learning; Pitman, London, 1988.Google Scholar
  12. [12]
    Y. Kodratoff: Proceedings of the 8th European Conference on Artificial Intelligence; August 1–5, Pitman, London, United Kingdom, 1988.Google Scholar
  13. [13]
    Z. Manna, R. Waldinger: A Deductive Approach to Program Synthesis; ACM Transactions on Programming Languages and Systems, Vol. 2., No.1, January, 1980, 90–121.CrossRefGoogle Scholar
  14. [14]
    R. Michalski, J. G. Carbonell, T. M. Mitchell (eds): Machine Learning: An Artificial Intelligence Approach; Tioga, Palo Alto, California, 1983.Google Scholar
  15. [15]
    T. M. Mitchell: Learning by experimentation, acquiring and refining problem-solving heuristics; in [14], 163–190.Google Scholar
  16. [16]
    H. Perdrix: Program synthesis from specifications; ESPRIT'85, Status Report of Continuing Work, North-Holland, 1986, 371–385.Google Scholar
  17. [17]
    D. R. Smith: Top-Down Synthesis of Simple Divide and Conquer Algorithm; Artificial Intelligence, vol. 27, no. 1, 1985, 43–96.CrossRefMathSciNetGoogle Scholar
  18. [18]
    M. Franova: Explanations in inductive theorem proving; to appear in Proceedings of the AAAI 90 Workshop on Learning.Google Scholar
  19. [19]
    G. DeJong, R. Mooney: Explanation-Based Learning: An Alternative View; Machine Learning 1, 1986, 145–176.Google Scholar
  20. [20]
    K. L. Clark, J. Darlington: Algorithm classification through synthesis; The Computer Journal, Vol. 23, No 1, 61–65.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Marta Fraňová
    • 1
  1. 1.CNRS & Université Paris SudOrsayFrance

Personalised recommendations