Complétude en Logiques

Résumé : Les travaux présentés succinctement dans ce mémoire concernent ce que l’on peut présenter en première lecture comme des démonstrations de la complétude des méthodes de démonstration automatique, en particulier de la méthode des tableaux. La complétude est un résultat permettant d’assurer que, si une assertion est prouvable – ou encore universellement valide–, alors la recherche de preuve exhaustive, associée à la méthode de démonstration automatique, aboutira. Comme nous le verrons, ces résultats de complétude se traduisent, tout d’abord, en des résultats de complétude sans coupure pour le calcul des séquents, puis en des théorèmes d’admissibilité de la coupure de ce même calcul des séquents, ce qui est l’un des résultats centraux de toute logique. Afin de l’obtenir dans un plus grand nombre de cas, nous développerons ensuite des méthodes plus algébriques. Nous approfondirons notre examen de ces démonstrations d’admissibilité de la coupure en les rapprochant des preuves de normalisation : dans un premier temps en étudiant la manière dont l’admissibilité, lorsqu’elle est démontrée de manière constructive, génère des preuves sans coupure, et donc contient un algorithme d’élimination des coupures. Dans un second temps, nous étudierons les structures sémantiques associées à la normalisation. Ces travaux ont été menés dans des systèmes logiques, tels que la logique d’ordre supérieure, classique, intuitionniste ou linéaire, en tenant compte de l’intentionnalité. Le domaine d’application le plus important des techniques développées dans ce manuscrit est cependant la Déduction modulo théorie, qui ajoute une relation de réécriture à la logique du premier ordre et aux systèmes de preuve. Cette relation permet de prendre en compte l’aspect calculatoire des preuves, et d’éviter l’introduction d’axiomes. L’étude de la règle de coupure et de son élimination devient uniforme ; de plus, l’on peut, jusqu’à un certain point, s’abstraire des systèmes de réécritures concret.
Mots-clés : Logique
Type de document :
HDR
Informatique [cs]. Université Paris Diderot (Paris 7), 2017
Liste complète des métadonnées

Littérature citée [135 références]  Voir  Masquer  Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/tel-01529422
Contributeur : Claire Medrala <>
Soumis le : mardi 30 mai 2017 - 17:53:52
Dernière modification le : vendredi 10 novembre 2017 - 14:54:43
Document(s) archivé(s) le : mercredi 6 septembre 2017 - 14:09:48

Identifiants

  • HAL Id : tel-01529422, version 1

Collections

Citation

Olivier Hermant. Complétude en Logiques. Informatique [cs]. Université Paris Diderot (Paris 7), 2017. 〈tel-01529422〉

Partager

Métriques

Consultations de la notice

795

Téléchargements de fichiers

121