Matrix-Based Inductive Theorem Proving

We present an approach to inductive theorem proving that integrates rippling-based rewriting into matrix-based logical proof search. The selection of appropriate connections in a matrix proof is guided by the symmetries between induction hypothesis and induction conclusion while unification is extended by a rippling/reverse-rippling heuristic. Conditional substitutions are generated whenever a uniform substitution is impossible. We illustrate the combined approach by discussing several inductive proofs for the integer square root problem.

• Type: Conference
• Year: 2000
• Where: TABLEAUX
• Authors: Christoph Kreitz, Brigitte Pientka
• Keywords: Artificial Intelligence, Inductive Theorem, Integer Square Root, Matrix-based Logical Proof, TABLEAUX 2000