Catalogue of Artificial Intelligence Techniques
Keywords: Nqthm, inductive learning, recursion
Categories: Theorem Proving
Author(s): Alan Bundy
This is a technique for constructing an appropriate rule of mathematical induction to prove a theorem. The standard form of mathematical induction is: P(0) n P(n) P(n+1)n P(n) but there are infinitely many such rules: for instance, there is one for each well ordering of each recursively defined data-structure. Thus applying induction presents an infinite branching point in a Search Space. Recursion analysis uses the definitions of the Recursive Functions in a theorem as a clue to the form of induction to be used to prove it. Each recursive definition suggests a dual induction rule. These suggestions are merged together to form an induction rule that subsumes as many of these recursive definitions as possible. This choice of induction rule improves the chances that the definitions of the recursive functions in the theorem can be used during the subsequent proofs of the base and step cases of the induction. Recursion analysis was invented by Boyer and Moore and implemented in their Nqthm inductive theorem prover. The best explanation can be found in the analysis by Stevens. Note: mathematical induction is a rule of deduction and is not to be confused with inductive learning, which is a rule of conjecture.
- Stevens, A., A Rational Reconstruction of Boyer and Moore's Technique for Constructing Induction Formulas Proceedings of ECAI-88 (1988), 565--570.