General purpose proof plans

  • Toby WalshEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 722)


One of the key problems in the design and implementation of automated reasoning systems is the specification of heuristics to control search. “Proof planning” has been developed as a powerful technique for declaratively specifying high-level proof strategies. This paper describes an extension to proof planning to allow for the specification of more general purpose plans.


General Purpose Conjunctive Normal Form Decision Class Proof Strategy Planning Language 
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. [Bun88]
    A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th Conference on Automated Deduction, pages 111–120. Springer-Verlag, 1988.Google Scholar
  2. [Bun91]
    A. Bundy. The use of proof plans for normalization. In R.S. Boyer, editor, Essays in Honor of Woody Bledsoe, pages 149–166. Kluwer, 1991.Google Scholar
  3. [BvHHS90]
    A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647–648. Springer-Verlag, 1990.Google Scholar
  4. [Fel89]
    A. Felty. Specifying and implementing theorem provers in a Higher Order Programming Language. PhD thesis, University of Pennsylvania, 1989.Google Scholar
  5. [GMW79]
    M.J. Gordon, A.J. Milner, and C.P. Wadsworth. Edinburgh LCF — A mechanised logic of computation, volume 78 of Lecture Notes in Computer Science. Springer Verlag, 1979.Google Scholar
  6. [TCS92]
    P. Traverso, A. Cimatti, and L. Spalazzi. Beyond the single planning paradigm: introspective planning. In Proceedings of the 9th ECAI, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  1. 1.Department of Artificial IntelligenceUniversity of EdinburghUK

Personalised recommendations