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.
Loading...