TY - GEN
T1 - A Rational Reconstruction and Extension of Recursion Analysis
AU - Bundy,Alan
AU - van Harmelen,F.
AU - Hesketh,J.
AU - Smaill,A.
AU - Stevens,A.
PY - 1989/8
Y1 - 1989/8
N2 - The focus of this paper is the technique of recur8\on analysis. Recursion analysis is used
by the Boyer-Moore Theorem Prover to choose
an appropriate induction schema and variable
to prove theorems by mathematical induction.
A rational reconstruction of recursion analysis
is outlined, using the technique of proof plans.
This rational reconstruction suggests an extension of recursion analysis which frees the induction suggestion from the forms of recursion
found in the conjecture. Preliminary results
are reported of the automation of this rational
reconstruction and extension using the CLAMOyster system.
AB - The focus of this paper is the technique of recur8\on analysis. Recursion analysis is used
by the Boyer-Moore Theorem Prover to choose
an appropriate induction schema and variable
to prove theorems by mathematical induction.
A rational reconstruction of recursion analysis
is outlined, using the technique of proof plans.
This rational reconstruction suggests an extension of recursion analysis which frees the induction suggestion from the forms of recursion
found in the conjecture. Preliminary results
are reported of the automation of this rational
reconstruction and extension using the CLAMOyster system.
M3 - Conference contribution
BT - Proceedings of the 11th International Joint Conference on Artificial Intelligence - IJCAI 1989
ER -