HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Inductive Proof Search Modulo

Fabrice Nahon 1 Claude Kirchner 1 Hélène Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system R and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system R,E has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationaly complete.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

Contributor : Helene Kirchner Connect in order to contact the contributor
Submitted on : Wednesday, November 14, 2007 - 10:15:44 PM
Last modification on : Friday, February 4, 2022 - 3:29:58 AM
Long-term archiving on: : Monday, September 24, 2012 - 3:26:09 PM


Files produced by the author(s)


  • HAL Id : inria-00187458, version 1



Fabrice Nahon, Claude Kirchner, Hélène Kirchner. Inductive Proof Search Modulo. 6th International Workshop on First-Order Theorem Proving - FTP 2007, Sep 2007, Liverpool, United Kingdom. pp.4-19. ⟨inria-00187458⟩



Record views


Files downloads