Preuves par induction dans le calcul des séquents modulo, Proof by induction in sequent calculus modulo

Fabrice Nahon

Description

Sous la direction de Claude Kirchner
Thèse soutenue le 26 octobre 2007: Nancy 1
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é.
-Déduction modulo
-Récurrence noethérienne
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.
Source: http://www.theses.fr/2007NAN10112/document

Informations

• Publié par: Thesee
• Nombre de lectures: 95
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

AVERTISSEMENT

Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.

Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.

Toute contrefaçon, plagiat, reproduction illicite encourt une
poursuite pénale.


➢ Contact SCD Nancy 1 : [e-mail]




LIENS


Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm Departement de formation doctorale en informatique Ecole doctorale IAEM Lorraine
UFR STMIA
Preuves par induction dans le calcul
des sequents modulo
THESE
presentee et soutenue publiquement le 26 Octobre 2007
pour l’obtention du
Doctorat de l’universite Henri Poincare { Nancy 1
(specialite informatique)
par
Fabrice Nahon
Composition du jury
President : Michael RUSINOWITCH Directeur de Recherche
Rapporteurs : Therese HARDIN Professeur
Toby WALSH
Examinateurs : Serge AUTEXIER Senior Researcher
Adel BOUHOULA Ma^ tre de Conferences
Adam CICHON Professeur
Claude KIRCHNER Directeur de Recherche
Helene KIR de Recherche
Michael RUSINOWITCH Directeur de Recherche
Laboratoire Lorrain de Recherche en Informatique et ses Applications | UMR 7503Mis en page avec la classe thloria.Remerciements
Il est temps pour moi de remercier tous ceux qui, de pres ou de loin, m’ont aide a realiser
ce travail. Tout d’abord, Claude et Helene Kirchner, qui ont etroitement encadre ce travail. Je
garde un excellent souvenir des entretiens tres reguliers et des echanges parfois tres animes que
nous avons eus ensemble. C’est sans doute gr^ ace a ces nombreuses discussions, ou j’ai toujours
ete ecoute et compris, que j’ai pris peu a peu con ance en moi et que j’ai pu commencer a
developper mes propres idees. Un long chemin a ete parcouru depuis le jour ou Claude m’a re cu
la premiere fois dans son bureau et m’a explique l’addition dans les entiers de Peano ! En e et,
je suis professeur (agrege) de mathematiques dans l’enseignement secondaire, et il m’a d’abord
fallu comprendre une copieuse litterature avant de pouvoir commencer un travail de recherche
en informatique. Celui-ci a vraiment debute quand Claude et Helene m’ont presente une ebauche
de systeme de recherche de preuve. Je devais determiner si on pouvait le corriger pour le rendre
correct. J’ai trouve la question claire et tres motivante. C’est en y repondant que d’autres se
sont posees au fur et a mesure, et que j’ai nalement ecrit cette these.
Je tiens ensuite a remercier vivement Therese Hardin, mon premier rapporteur, pour l’inter^et
qu’elle a immediatement manifeste pour ce travail quand je l’ai rencontree pour lui presenter
le manuscrit. Ses remarques, aussi bien ecrites qu’orales, ont ete d’une part une aide precieuse
pour rediger la version nale du document, et contiennent d’autre part de nombreuses pistes
pour prolonger la re exion. Je suis aussi tres reconnaissant a Toby Walsh d’avoir accepte, depuis
l’Australie, d’^etre egalement rapporteur. Son regard sur le manuscrit m’a ete tres utile pour le
preciser et parfois le corriger. J’ai par ailleurs ete tres honore que mon jury ait compte autant
de chercheurs de renom, dont les ouvrages et articles ont inspire cette these. Leurs nombreuses
questions et remarques au cours de la soutenance m’ont en outre bien renseigne sur les nouvelles qui se posent a la suite de mes recherches .
Je remercie aussi chaleureusement les membres de l’equipe protheo (notamment Eric Deplagne,
dont la these est a l’origine de ce travail, et qui m’a egalement de nombreuses fois \depanne"
lorsque l’ordinateur ne reagissait pas comme je voulais ), avec lesquels j’ai travaille dans une
ambiance tres detendue, ainsi que Chantal Llorens, qui a beaucoup compte pour les questions
d’ordre administratif. Et en n, je ne dois pas oublier mes proches : mes parents, auxquels je me
suis souvent con e et qui qui m’ont beaucoup soutenu tout au long de ce parcours, ainsi que
Bettina, ma femme, qui a accepte que je consacre autant de mon temps libre a ce qu’elle appelle
mes formules !
iiiA Bettina, ma femme, a mes parents, et a mon frere Emmanuel, handicape.
iiiivTable des matieres
Introduction generale xiii
1 Necessite de la recurrence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiii
2 Les di erents principes de recurrence . . . . . . . . . . . . . . . . . . . . . . xvi
3 Recurrence et demonstration automatique . . . . . . . . . . . . . . . . . . . . xvii
4 Motivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xviii
5 Plan de la these . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xx
Partie I Notions fondamentales 1
Chapitre 1
Cadre general
1.1 Le paysage syntaxique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.1.1 Mots . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.1.2 Termes nis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.1.3 Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.1.4 Propositions du premier ordre . . . . . . . . . . . . . . . . . . . . . . 12
1.2 Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2.1 Logique du premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2.2 Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.3 Le paysage semantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.3.1 Interpretation d’une signature fonctionnelle . . . . . . . . . . . . . . . 18
1.3.2 Les algebres de termes . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.3.3 Interpretation des symboles relationnels . . . . . . . . . . . . . . . . . 20
1.4 Satisfaction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.4.1 Consequence semantique . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.4.2 Consequence inductive . . . . . . . . . . . . . . . . . . . . . . . . . . 22
vTable des matieres
Chapitre 2
Reecriture
2.1 Relation binaire sur un ensemble . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2 Systeme de reecriture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.2.1 Cas non conditionnel . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.2.2 Cas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.3 Speci cation equationnelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.3.1 Un systeme de reecriture particulier . . . . . . . . . . . . . . . . . . . 30
2.3.2 Pourquoi orienter les egalites ? . . . . . . . . . . . . . . . . . . . . . . 31
2.3.3 Uni cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.3.4 Paires critiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.3.5 La procedure de completion de Knuth-Bendix . . . . . . . . . . . . . 34
2.4 Completude su sante . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
2.5 Reecriture modulo un ensemble d’egalites . . . . . . . . . . . . . . . . . . . . 36
2.5.1 Relation binaire modulo un ensemble d’egalites . . . . . . . . . . . . . 36
2.5.2 ReecritureR;E et completude su sante . . . . . . . . . . . . . . . . 37
Chapitre 3
Preuves automatiques par recurrence
3.1 Preuves par consistance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.2 Preuves par recurrence explicite . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.3 Preuves par r implicite . . . . . . . . . . . . . . . . . . . . . . . . . 50
3.4 Recurrence et deduction modulo . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.4.2 Le mecanisme de la deduction modulo . . . . . . . . . . . . . . . . . . 54
3.4.3 Recurrence dans le contexte de la deduction modulo . . . . . . . . . . 56
3.5 Descente in nie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
Partie II Ordre et surreduction : deux outils principaux pour la
methode 61
Chapitre 1
Ordres et quasi-ordres
1.1 Ordre sur les termes et terminaison des systemes de reecriture . . . . . . . . 63
1.2 Ordres et quasi-ordres sur les chemins . . . . . . . . . . . . . . . . . . . . . . 66
1.3 Ordres et sur les egalites . . . . . . . . . . . . . . . . . . . . . . 67
vi1.4 Ordres recursifs sur les chemins AC-compatibles . . . . . . . . . . . . . . . . 70
1.4.1 Termes variadiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
1.4.2 Construction d’un ordre recursif sur les chemins AC-compatible . . . 72
Chapitre 2
Surreduction
2.1 Principe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
2.2 Surreduction modulo un ensemble d’egalites . . . . . . . . . . . . . . . . . . 76
2.3 Surr et completude su sante . . . . . . . . . . . . . . . . . . . . . . 78
2.3.1 Uni cateurs constructeurs . . . . . . . .