La lecture à portée de main
Découvre YouScribe en t'inscrivant gratuitement
Je m'inscrisDécouvre YouScribe en t'inscrivant gratuitement
Je m'inscrisDescription
Informations
Publié par | Thesee |
Nombre de lectures | 24 |
Langue | Français |
Poids de l'ouvrage | 2 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.
D’autre part, 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 UFR STMIA École doctorale IAEM Lorraine
Département de formation doctorale en informatique
Bonnes démonstrations
en déduction modulo
THÈSE
présentée et soutenue publiquement le 23 mars 2009
pour l’obtention du
doctorat de l’université Henri POINCARÉ
(spécialité informatique)
par
Guillaume Burel
Composition du jury
Président : Delia Kesner Professeur, université Denis Diderot, Paris, France
Rapporteurs : Nachum Dershowitz Professeur, université de Tel Aviv, Israël
Gilles Dowek Professeur, École polytechnique, Palaiseau, France
Examinateurs : Patrick Blackburn Directeur de recherche, Inria, Nancy, France
Claude Kirchner Directeur de recherche, Inria, Bordeaux, France (directeur de thèse)
Daniel Leivant Professeur, université de l’Indiana, Bloomington, ÉUA
Dominique Mery Professeur, université Henri Poincaré, Nancy, France
Alexandre Miquel Maître de conférences, université Denis Diderot, Paris, France
Laboratoire Lorrain de recherche en informatique et ses applications — UMR 7503AMis en page avec LT X.E
L’œuvre de RandallMunroe reproduite page 183 est sous licence Creative Commons
paternité–pas d’utilisation commerciale 2.5.Remerciements
Je tiens à exprimer ma reconnaissance envers toutes les personnes grâce auxquelles
ces trois années (et demi) de thèse se sont déroulées si plaisamment. Mes premiers
remerciements sont évidemment pour mon directeur de thèse, Claude Kirchner, qui,
il y a bientôt six ans de cela, et avec Olivier Bournez, me fit découvrir le monde de la
recherche.Jetiensàsoulignersadisponibilité,surtoutendébutdethèseoùsacapacitéà
pointer des références intéressantes m’a été précieuse et où il m’a encouragé et aidé dans
les différentes pistes que j’ai explorées. Si ses nouvelles responsabilités, et surtout son
nouveau lieu de travail, ont bien entendu réduit la possibilité d’interactions scientifiques
régulières,ilavaitdéjàdonnél’impulsionnécessairequim’apermisd’accomplirletravail
décrit dans ce manuscrit, et il a su être disponible aux moments nécessaires.
Je souhaite aussi remercier tous les membres qui m’ont fait l’honneur d’accepter de
faire partie de mon jury de soutenance. Répondre à leurs pertinentes questions me don-
nera du travail pour longtemps. Merci spécialement à Nachum Dershowitz et à Gilles
Dowek d’avoir accepté de rapporter ce manuscrit. J’apprécie également leur intérêt
constant pour mon travail.
Grand merci à tous les membres et anciens membres des équipes Prothéo puis Paréo.
La bonne ambiance qui y règne favorise grandement les échanges et donc les avancées
scientifiques. Merci en particulier à ceux que j’ai côtoyés alors qu’ils étaient encore thé-
sards : Benjamin, Clara, Antoine, Florent, Fabrice, Germain, Colin, Anderson, Radu,
Oana et Émilie. Merci à ceux qui auront bientôt à remplir une telle page : Clément,
Paul, Cody, Claudia et Tony. Merci aussi à Jean-Christophe avec qui j’ai partagé le
bureau vers la fin, à Pierre-Étienne qui dirige Paréo admirablement, à Hélène, Frédé-
ric, Horatiu et Yves, et surtout à Chantal qui sait combattre efficacement les hydres
administratives.
J’aimerais également remercier tous ceux qui travaillent ou ont travaillé autour de la
déduction modulo et qui ont pu apporter un regard critique sur mes avancées : Claude
et Gilles, que j’ai déjà cités, mais également Thérèse, Benjamin, Alexandre, Olivier,
Richard, Denis, Lisa et Mathieu. Merci aussi aux personnes qui m’ont accompagné au
cours de mes études : Rémi, Christophe, Gim, David, Samuel, Florent, Laurent et tous
les autres.
Je voudrais témoigner ma gratitude envers ceux qui, volontairement ou non, m’ont
fortement influencé : Herr Krameyer qui a inclinée durablement ma Weltanschauung,
Kai qui m’a ouvert à de nouveaux horizons et M. Soyeur grâce à qui j’ai découvert
ce que sont les mathématiques et l’informatique théorique. Je remercie également mes
iRemerciements
parents et ma sœur qui m’ont toujours soutenu en me laissant libre de mes choix. Ces
remerciements seraient néanmoins incomplets s’ils n’étaient en grande partie adressés à
Céline, qui a pourtant tort de croire plus en moi qu’en elle-même.
Merci à ceux que j’aurais pu oublier, j’espère qu’ils ne s’en formaliseront pas.
Je remercie enfin tous ceux qui savent associer réécriture et beauté.
iiTable des matières
Extended abstract 1
1 Introduction 5
Plan de la thèse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2 Notions préliminaires 17
2.1 Notions mathématiques de base . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2 Logique(s) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.2.1 Logique du premier ordre . . . . . . . . . . . . . . . . . . . . . . . 24
2.2.2es d’ordre supérieur. . . . . . . . . . . . . . . . . . . . . . . 27
2.3 Systèmes de déduction pour la logique du premier ordre . . . . . . . . . . 29
2.3.1 Systèmes d’inférence . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.3.2 Systèmes schématiques . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.3.3 Déduction naturelle . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.3.4 Calculs des séquences . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.3.5 Traductions entre calcul des séquences et déduction naturelle . . . 49
3 Démonstration et calcul 57
3.1 Identifier démonstration et calcul . . . . . . . . . . . . . . . . . . . . . . . 57
3.1.1 Interprétation de Heyting-Brouwer-Kolmogorov . . . . . . . 57
3.1.2 Isomorphisme de Curry-Howard . . . . . . . . . . . . . . . . . . 58
3.1.3 Extension : les systèmes de type purs . . . . . . . . . . . . . . . . 61
3.2 Déduction modulo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
3.2.1 Variations sur les systèmes de déduction modulo . . . . . . . . . . 73
3.2.2 Sémantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
3.2.3 Admissibilité des coupures en déduction modulo . . . . . . . . . . 81
3.2.4 Méthodes de recherches de démonstration basées sur la déduction
modulo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
3.3 Surdéduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
3.3.1 Déduction surnaturelle . . . . . . . . . . . . . . . . . . . . . . . . . 91
3.3.2 Calcul des séquences extensible . . . . . . . . . . . . . . . . . . . . 101
3.3.3 Propriétés des systèmes de surdéduction intuitionnistes . . . . . . 111
iiiTable des matières
4 Complétion abstraite pour l’obtention de l’admissibilité des coupures 115
4.1 Exemple introductif . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
4.2 Systèmes canoniques abstraits . . . . . . . . . . . . . . . . . . . . . . . . . 118
4.2.1 Définitions et postulats . . . . . . . . . . . . . . . . . . . . . . . . 118
4.2.2 Mécanismes de complétion. . . . . . . . . . . . . . . . . . . . . . . 120
4.3 Le calcul des séquences avec dépliage polarisé comme instance de système
canonique abstrait . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
4.3.1 Système de réécriture et séquence . . . . . . . . . . . . . . . . . . . 122
4.3.2 Démonstrations, formules, ordres . . . . . . . . . . . . . . . . . . . 129
4.3.3 Procédure de complétion. . . . . . . . . . . . . . . . . . . . . . . . 133
4.3.4 Exemples d’applications . . . . . . . . . . . . . . . . . . . . . . . . 138
4.4 Implémentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
4.4.1 TOM/OCaml . . . . . . . . . . . . . . . . . . . . .