Matrixbased Inductive Theorem Proving


Christoph Kreitz, Brigitte Pientka.  
In R. Dyckhoff, ed., International Conference TABLEAUX2000, LNAI 1847, pp. 294308, Springer Verlag, 2000. 

Abstract 

We present an approach to inductive theorem proving that integrates
ripplingbased rewriting into matrixbased 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/reverserippling
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 = "Matrixbased Inductive Theorem Proving", booktitle = "International Conference TABLEAUX2000", year = "2000", editor = "R. Dyckhoff", volume = "1847", series = "Lecture Notes in Artificial Intelligence", pages = "294308", publisher = "Springer Verlag" } 