Studia Logica 69 (2):293-326 (2001)
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.
|Keywords||Philosophy Logic Mathematical Logic and Foundations Computational Linguistics|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Deductively Definable Logies of Induction.John Norton - 2010 - Journal of Philosophical Logic 39 (6):617 - 654.
Connection Tableau Calculi with Disjunctive Constraints.Ortrun Ibens - 2002 - Studia Logica 70 (2):241 - 270.
On Automating Diagrammatic Proofs of Arithmetic Arguments.Mateja Jamnik, Alan Bundy & Ian Green - 1999 - Journal of Logic, Language and Information 8 (3):297-321.
Added to index2009-01-28
Total downloads15 ( #309,090 of 2,154,092 )
Recent downloads (6 months)1 ( #398,005 of 2,154,092 )
How can I increase my downloads?