General purpose proof plans
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.
KeywordsGeneral Purpose Conjunctive Normal Form Decision Class Proof Strategy Planning Language
Unable to display preview. Download preview PDF.
- [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
- [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
- [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
- [Fel89]A. Felty. Specifying and implementing theorem provers in a Higher Order Programming Language. PhD thesis, University of Pennsylvania, 1989.Google Scholar
- [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
- [TCS92]P. Traverso, A. Cimatti, and L. Spalazzi. Beyond the single planning paradigm: introspective planning. In Proceedings of the 9th ECAI, 1992.Google Scholar