Inductive Proof Search Modulo - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2007

Inductive Proof Search Modulo

Résumé

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.
Fichier principal
Vignette du fichier
ftp-07.pdf (219.52 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00187458 , version 1 (14-11-2007)

Identifiants

  • HAL Id : inria-00187458 , version 1

Citer

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⟩
238 Consultations
103 Téléchargements

Partager

Gmail Facebook X LinkedIn More