ConnectionDriven Inductive Theorem Proving


Christoph Kreitz, Brigitte Pientka.  
Studia Logica 69(2):293326, 2001. 

Abstract 

We present a method for integrating ripplingbased rewriting
into matrixbased 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/reverserippling 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 = "ConnectionDriven Inductive Theorem Proving", journal = "Studia Logica", year = "2001", volume = 69, number = 2, pages = "293326" } 