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.
Type de document :
Communication dans un congrès
Silvio Ranise. 6th International Workshop on First-Order Theorem Proving - FTP 2007, Sep 2007, Liverpool, United Kingdom. Technical report ULCS-07-018 Department of Computer Science University of Liverpool, pp.4-19, 2007, Proceedings of the 6th International Workshop on First-Order Theorem Proving FTP 2007
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00187458
Contributeur : Helene Kirchner <>
Soumis le : mercredi 14 novembre 2007 - 22:15:44
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : lundi 24 septembre 2012 - 15:26:09

Fichier

ftp-07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00187458, version 1

Collections

Citation

Fabrice Nahon, Claude Kirchner, Hélène Kirchner. Inductive Proof Search Modulo. Silvio Ranise. 6th International Workshop on First-Order Theorem Proving - FTP 2007, Sep 2007, Liverpool, United Kingdom. Technical report ULCS-07-018 Department of Computer Science University of Liverpool, pp.4-19, 2007, Proceedings of the 6th International Workshop on First-Order Theorem Proving FTP 2007. 〈inria-00187458〉

Partager

Métriques

Consultations de la notice

213

Téléchargements de fichiers

94