TY - GEN
T1 - The Use of Explicit Plans to Guide Inductive Proofs
AU - Bundy, Alan
PY - 1988/5
Y1 - 1988/5
N2 - We propose the use of explicit proof plans to guide the search for a proof in automatic theorem proving. By representing proof plans as the specifications of LCF-like tactics, [Gordon et al 79], and by recording these specifications in a sorted meta-logic, we are able to reason about the conjectures to be proved and the methods available to prove them. In this way we can build proof plans of wide generality, formally account for and predict their successes and failures, apply them flexibly, recover from their failures, and learn them from example proofs.
We illustrate this technique by building a proof plan based on a simple subset of the implicit proof plan embedded in the Boyer-Moore theorem prover, [Boyer & Moore 79].
AB - We propose the use of explicit proof plans to guide the search for a proof in automatic theorem proving. By representing proof plans as the specifications of LCF-like tactics, [Gordon et al 79], and by recording these specifications in a sorted meta-logic, we are able to reason about the conjectures to be proved and the methods available to prove them. In this way we can build proof plans of wide generality, formally account for and predict their successes and failures, apply them flexibly, recover from their failures, and learn them from example proofs.
We illustrate this technique by building a proof plan based on a simple subset of the implicit proof plan embedded in the Boyer-Moore theorem prover, [Boyer & Moore 79].
KW - Proof plans
KW - inductive proofs
KW - theorem proving
KW - automatic programming
KW - formal methods
KW - planning
U2 - 10.1007/BFb0012826
DO - 10.1007/BFb0012826
M3 - Conference contribution
SN - 978-3-540-19343-2
T3 - Lecture Notes in Computer Science
BT - 9th International Conference on Automated Deduction
PB - Springer-Verlag GmbH
ER -