Connection-Driven Inductive Theorem Proving
Christoph Kreitz, Brigitte Pientka.
Studia Logica 69(2):293-326, 2001.
Abstract
	We present a method for integrating rippling-based rewriting into matrix-based theorem proving as a means for automating inductive specification proofs. The selection of connections in an inductive matrix proof is guided by symmetries between induction hypothesis and induction conclusion. Unification is extended by decision procedures and a rippling/reverse-rippling heuristic. Conditional substitutions are generated whenever a uniform substitution is impossible. We illustrate the integrated method by discussing several inductive proofs for the integer square root problem as well as the algorithms extracted from these proofs.

		(Preprint)	Back to overview of papers
Bibtex Entry
	@Article{ar:KreitzPientka01a, author = "Christoph Kreitz and Brigitte Pientka", title = "Connection-Driven Inductive Theorem Proving", journal = "Studia Logica", year = "2001", volume = 69, number = 2, pages = "293--326" }