TY - JOUR
T1 - Experiments with Proof Plans for Induction
AU - Bundy, Alan
AU - van Harmelen, F.
AU - Hesketh, J.
AU - Smaill, A.
PY - 1991
Y1 - 1991
N2 - The technique of proof plans, is outlined. This technique is used to guideautomatic inference in order to avoid a combinatorial explosion. Empirical research to test this technique in the domain of theorem proving by mathematical induction is described. Heuristics, adapted from the work of Boyer and Moore, have been implemented as Prolog programs, called tactics, and used to guide an inductive proof checker, Oyster. These tactics have been partially specied in a meta-logic, and plan formation has been used to reason with these specications and form plans. These plans are then executed by running their associated tactics and, hence, performing an Oyster proof. Results are presented of the use of this technique on a number of standard theorems from the literature. Searching in the planning space is shown to be considerably cheaper than searching directly in Oyster's search space. The success rate on the standard theorems is high. These preliminary results are very encouraging.
AB - The technique of proof plans, is outlined. This technique is used to guideautomatic inference in order to avoid a combinatorial explosion. Empirical research to test this technique in the domain of theorem proving by mathematical induction is described. Heuristics, adapted from the work of Boyer and Moore, have been implemented as Prolog programs, called tactics, and used to guide an inductive proof checker, Oyster. These tactics have been partially specied in a meta-logic, and plan formation has been used to reason with these specications and form plans. These plans are then executed by running their associated tactics and, hence, performing an Oyster proof. Results are presented of the use of this technique on a number of standard theorems from the literature. Searching in the planning space is shown to be considerably cheaper than searching directly in Oyster's search space. The success rate on the standard theorems is high. These preliminary results are very encouraging.
KW - Theorem proving
KW - mathematical induction
KW - search
KW - Combinatorial explosion
KW - Proof plans
KW - tactics
KW - Planning
U2 - 10.1007/BF00249016
DO - 10.1007/BF00249016
M3 - Article
VL - 7
SP - 303
EP - 324
JO - Journal of Automated Reasoning
T2 - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
SN - 0168-7433
IS - 3
ER -