Bonnes démonstrations en déduction modulo, Good proofs in deduction modulo
267 pages
Français

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Bonnes démonstrations en déduction modulo, Good proofs in deduction modulo

-

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
267 pages
Français
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Sous la direction de Claude Kirchner
Thèse soutenue le 23 mars 2009: Nancy 1
Cette thèse étudie comment l'intégration du calcul dans les démonstrations peut les simplifier. Nous nous intéressons pour cela à la déduction modulo et à la surdéduction, deux formalismes proches dans lesquels le calcul est incorporé dans les démonstrations via un système de réécriture. Pour améliorer la recherche mécanisée de démonstration, nous considérons trois critères de simplicité. L'admissibilité des coupures permet de restreindre l'espace de recherche des démonstrations, mais elle n'est pas toujours assurée en déduction modulo. Nous définissons une procédure qui complète le système de réécriture pour, au final, admettre les coupures. Au passage, nous montrons comment transformer toute théorie pour l'intégrer à la partie calculatoire des démonstrations. Nous montrons ensuite comment la déduction modulo permet de réduire arbitrairement la taille des démonstrations, en transférant des étapes de déduction dans le calcul. En particulier, nous appliquons ceci à l'arithmétique d'ordre supérieur pour démontrer que les réductions de taille qui sont possibles en augmentant l'ordre dans lequel on se place disparaissent si on travaille en déduction modulo. Suite à ce dernier résultat, nous avons recherchés quels sont les systèmes d'ordre supérieur pouvant être simulés au premier ordre, en déduction modulo. Nous nous sommes intéressés aux systèmes de type purs et nous montrons comment ils peuvent être encodés en surdéduction, ce qui offre de nouvelles perspectives concernant leur normalisation et la recherche de démonstration dans ceux-ci. Nous développons également une méthodologie qui permet d'utiliser la surdéduction pour spécifier des systèmes de déduction.
-Ordre sur les démonstrations
This thesis study how computations may simplify proofs and aims to make mechanized proof search better. We are particularly interested in deduction modulo and superdeduction, two close formalisms allowing the integration of computations into proofs through a rewrite system. We consider three simplicity criteria related to proof search. Cut admissibility makes it possible to restrain the proof-search space but does not always hold in deduction modulo. We define a completion method transforming a rewrite system representing computations so that at the end cut admissibility holds. By the way, we show how to transform any first-order theory to integrate it into the computational part of proofs. We show then how deduction modulo unboundedly reduces proof lengths, by transferring deduction steps into computations. In particular, we apply this to higher-order arithmetic to show that proof-length speedups between ith- and i+1st-order arithmetic disappear when working in deduction modulo, making it possible to work in first-order logic modulo without increasing proof lengths. Following this last result, we investigate which higher-order systems can be simulated in first order using deduction modulo. We are interested by pure type systems, which are generic type systems for the lambda-calculus with dependent types. We show how these systems can be encoded in superdeduction. This offers new perspectives on their normalization and on proof search within them. We also develop a methodology to describe how superdeduction can be used to specify deductive systems.
Source: http://www.theses.fr/2009NAN10014/document

Informations

Publié par
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 . . . . . . . . . . . . . . . . . . . . .

  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents