Matrix-based Inductive Theorem Proving

Christoph Kreitz, Brigitte Pientka.

In R. Dyckhoff, ed., International Conference TABLEAUX-2000,
LNAI 1847, pp. 294-308, Springer Verlag, 2000.


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.

Paper is available in
postscript and pdf format
  Slides of the conference presentation are available in compressed postscript and pdf format
The talk includes a separate PowerPoint animation

Bibtex Entry

Back to overview of papers
@InProceedings{inp:KreitzPientka00a, author = ""Christoph Kreitz and Brigitte Pientka", title = "Matrix-based Inductive Theorem Proving", booktitle = "International Conference TABLEAUX-2000", year = "2000", editor = "R. Dyckhoff", volume = "1847", series = "Lecture Notes in Artificial Intelligence", pages = "294--308", publisher = "Springer Verlag" }