229
pages
Français
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe en t'inscrivant gratuitement
Découvre YouScribe en t'inscrivant gratuitement
229
pages
Français
Ebook
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
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 : theses.sciences@scd.uhp-nancy.fr
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 . . . . . . . .