Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #886 | |
|---|---|
| Title: | Proof Planning |
| Authors: | Bundy,A |
| Date: | Jan 1998 |
| Presented: | Published in the Proceedings of the 3rd International Conference on AI Planning Systems, 1996 |
| Keywords: | |
| Abstract: | We describe proof planning, a technique for the global control of search in automatic theorem proving. A proof plan captures the common patterns of reasoning in a family of similar proofs and is used to guide the search for new proofs in this family. Proof plans are very similar to the plans constructed by plan formation techniques. Some differences are the non-persistence of objects in the mathematical domain, the absence of goal interaction in mathematics, the high degree of generality of proof plans, the use of a meta-logic to describe preconditions in proof planning and the use of annotations in formulae to guide search. |
| Download: | POSTSCRIPT COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}