Proof plans for the correction of false conjectures

  • Raul Monroy
  • Alan Bundy
  • Andrew Ireland
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 822)


Theorem proving is the systematic derivation of a mathematical proof from a set of axioms by the use of rules of inference. We are interested in a related but far less explored problem: the analysis and correction of false conjectures, especially where that correction involves finding a collection of antecedents that, together with a set of axioms, transform non-theorems into theorems. Most failed search trees are huge, and special care is to be taken in order to tackle the combinatorial explosion phenomenon. Fortunately, the planning search space generated by proof plans, see [1], are moderately small. We have explored the possibility of using this technique in the implementation of an abduction mechanism to correct non-theorems.


Induction Hypothesis Inductive Proof Planning Critic Automate Deduction Recursive Definition 
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.
    Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In 9th Conference on Automated Deduction. Lusk, R. and Overbeek, R.(Eds.). (1988) 111–120. Longer version available from Edinburgh as DAI Research Paper No. 349.Google Scholar
  2. 2.
    Bundy, A. and van Harmelen, F. and Hesketh, J. and Smaill, A.: Experiments with Proof Plans for Induction. Journal of Automated Reasoning 7 (1991) 303–324.Google Scholar
  3. 3.
    Bundy, A. and van Harmelen, F. and Horn, C. and Smaill, A.: The Oyster-Clam system. In Proceedings of the 10th International Conference on Automated Deduction. Springer-Verlag. Stickel, M.E. (Ed.). (1990) 647–648.Google Scholar
  4. 4.
    Bundy, A. and Stevens, A. and van Harmelen, F. and Ireland, A. and Smaill, A.: Rippling: A Heuristic for Guiding Inductive Proofs. Artificial Intelligence 62 (1993) 182–253.Google Scholar
  5. 5.
    Cox, P.T. and Pietrzykowski, T.: Causes for Events: Their Computation and Applications. Lecture Notes in Computer Science: Proceedings of the 8th International Conference on Automated Deduction. Siekmann, J. (Ed.) Springer-Verlag. (1986) 608–621.Google Scholar
  6. 6.
    Finger, J.J.:RESIDUE: A deductive approach to design synthesis. Research Report STAN-CS-85-1035. Stanford University (1985).Google Scholar
  7. 7.
    Franova, M. and Kodratoff, Y.: Predicate Synthesis from Formal Specifications. Proceedings of ECAI-92. (1992) 87–91.Google Scholar
  8. 8.
    Gordon, M.J. and Milner, A.J. and Wadsworth, C.P.: Edinburgh LCF — A mechanised logic of computation. Lecture Notes in Computer Science 78 (1979).Google Scholar
  9. 9.
    Ireland, A.: The Use of Planning Critics in Mechanizing Inductive Proofs. International Conference on Logic Programming and Automated Reasoning — LPAR 92, St. Petersburg. Lecture Notes in Artificial Intelligence 624. Voronkov A. (Ed.). Springer-Verlag. (1992) 178–189.Google Scholar
  10. 10.
    Ireland, A. and Bundy, A.: Using Failure to Guide Inductive Proof. Technical Report, Department of Artificial Intelligence (1992). Available from Edinburgh as DAI Research Paper 613.Google Scholar
  11. 11.
    Monroy, R.: Abduction Mechanisms. Working Paper No. 254, Department of Artificial Intelligence, Edinburgh Univerisity (1994).Google Scholar
  12. 12.
    Paul, G.: Approaches to Abductive Reasoning: an Overview. Artificial Intelligence Review, vol. 7, 109–152. Kluwer Academic Publisher (1993).Google Scholar
  13. 13.
    Peirce, C.S.: Collected papers of Charles Sanders Peirce. Vol. 2, 193. Harston, C. and Weiss, P. (Eds.) Harvard University Press. (1959).Google Scholar
  14. 14.
    Poole, G. and Goebel, R. and Aleliunas, R.: Theorist: a logical reasoning system for defaults and diagnosis. The Knowledge Frontier: Essays in Representation of Knowledge. Cercone, N. and McCalla, G. (Eds.), Springer-Verlag (1987) 331–352.Google Scholar
  15. 15.
    Pople, H.E.: On the Mechanization of Abductive Logic. Proceedings of the third IJCAI. Nilsson, N. (Ed.). (1972) 147–152.Google Scholar
  16. 16.
    Selman, B. and Levesque, H.L.: Abductive and Default Reasoning: A Computational Core. In Proccedings of the 8th National Conference on Artificial Intelligence. (1989) 343–348.Google Scholar
  17. 17.
    van Harmelen, F.: The CLAM Proof Planner, User Manual and Programmer Manual. Technical Paper 4. Department of Artificial Intelligence, Edinburgh University. 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Raul Monroy
    • 1
  • Alan Bundy
    • 1
  • Andrew Ireland
    • 1
  1. 1.Department of Artificial IntelligenceThe University of EdinburghScotlandUK

Personalised recommendations