Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

Recursion Analysis

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.



Add Comment

No comments.