Proof by induction in sequent calculus modulo

Preuve par induction dans le calcul des séquents modulo

Fabrice Nahon (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs

We are presenting an original narrowing-based proof search method for inductive theorems. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemes. It also yields a direct translation from a successful proof search derivation to a proof in the sequent calculus. The method is shown to be correct and refutationally complete in a proof theoretical way. We are extending this first approach to equational rewrite theories given by a rewrite system R and a set E of equalities. Whenever the equational rewrite system (R,E) has good properties of termination, sufficient completeness, and whenever E is constructor preserving, narrowing at defined-innermost positions is performed with unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined.

Nous présentons une méthode originale de recherche de preuve par récurrence utilisant la surréduction. Elle a la particularité d'être fondée sur la déduction modulo et d'utiliser la surréduction pour sélectionner à la fois les variables de récurrence et les schémas d'instanciation. Elle donne également la possibilité de traduire directement toute dérivation effectuée avec succès en une preuve dans le calcul des séquents modulo. La correction et la complétude réfutationnelle de la méthode sont démontrées en théorie de la preuve. Nous étendons ensuite cette première approche aux théories de réécriture équationnelles constituées d'un système de réécriture R et d'un ensemble E d'égalités. A partir du moment où le système de réécriture équationnel (R,E) possède de bonnes propriétés de terminaison et de complétude suffisante, et si on suppose également que E préserve les constructeurs, la surréduction au niveau des positions les plus profondes où apparaît un symbole défini s'effectue uniquement à l'aide d'unificateurs qui sont également des substitutions constructeurs. Ceci est particulièrement intéressant dans le cas des théories associatives, ou associatives commutatives, pour lesquelles notre système de recherche de preuve a été raffiné.

Mots clés: sequent calculus modulo; induction; Noetherian induction; induction by rewriting; equational reasoning; term rewriting; equational rewriting; equational narrowing

Mots clés: Déduction modulo; calcul des séquents modulo; récurrence; récurrence noethérienne; récurrence par réécriture; raisonnement équationnel; réécriture de termes; réécriture équationnelle; surréduction équationnelle

Domaines: Autre [cs.OH]

Fabrice Nahon. Preuve par induction dans le calcul des séquents modulo. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2007. Français. ⟨NNT : ⟩. ⟨tel-01748243v3⟩