Inductive Proof Search Modulo

Fabrice Nahon 1 Claude Kirchner 1, 2 Hélène Kirchner 1, 2 Paul Brauner 1
1 PAREO - Formal islands: foundations and applications
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 correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.
Type de document :
Article dans une revue
Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2009, Special Issue on First-Order Theorem Proving / Guest Edited by Silvio Ranise and Ullrich Hustadt, 55 (1), pp.123-154. 〈10.1007/s10472-009-9154-5〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00337380
Contributeur : Paul Brauner <>
Soumis le : jeudi 6 novembre 2008 - 17:40:44
Dernière modification le : jeudi 11 janvier 2018 - 01:49:21
Document(s) archivé(s) le : mardi 9 octobre 2012 - 15:05:32

Fichier

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

Identifiants

Collections

Citation

Fabrice Nahon, Claude Kirchner, Hélène Kirchner, Paul Brauner. Inductive Proof Search Modulo. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2009, Special Issue on First-Order Theorem Proving / Guest Edited by Silvio Ranise and Ullrich Hustadt, 55 (1), pp.123-154. 〈10.1007/s10472-009-9154-5〉. 〈inria-00337380〉

Partager

Métriques

Consultations de la notice

221

Téléchargements de fichiers

123