Connection-driven inductive theorem proving
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. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,865 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesMatthias Hild (2006). Inductive Incompleteness. Philosophical Studies 128 (1):109 - 135.
Ortrun Ibens (2002). Connection Tableau Calculi with Disjunctive Constraints. Studia Logica 70 (2):241 - 270.
David Harriman (2010). The Logical Leap: Induction in Physics. New American Library.
John D. Norton (2003). A Material Theory of Induction. Philosophy of Science 70 (4):647-670.
Mateja Jamnik, Alan Bundy & Ian Green (1999). On Automating Diagrammatic Proofs of Arithmetic Arguments. Journal of Logic, Language and Information 8 (3):297-321.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2009-01-28Total downloads0Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
