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.
Abstract
	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" }