Directeur:
Pr.
Gilles Dowek
Composition du Jury:
Pr.
Thierry Coquand (rapporteur)
Pr.
Mitsuhiro Okada (rapporteur)
Pr.
Jean Goubault-Larrecq
Pr.
Thérèse Hardin (pr\'esident)
Pr.
Delia Kesner
Pr.
James Lipton
Soutenue le 6 Décembre 2005
Résumé:
La Déduction Modulo est un formalisme logique qui
intègre des étapes de déduction et des étapes de calcul, sous
la forme de règles de réécriture. On obtient ainsi un calcul
plus souple, plus adapté à la démonstration automatique, plus
lisible pour un être humain. Une conséquence remarquable est qu'il
permet d'exprimer beaucoup de théories axiomatiques avec des
règles de calcul.
L'une des propriétés étudiée dans cette thèse est
l'élimination des coupures. Elle est capitale car elle implique la
cohérence du système considéré, et permet l'implantation
effective d'algorithmes de recherche de preuve. Or, en Déduction
Modulo, cette propriété n'est pas vraie pour tous les systèmes
de réécriture, mais seulement dans certains. Ceci amène à
rechercher les systèmes vérifiant l'élimination
des coupures.
Cette thèse introduit tout d'abord les outils
sémantiques permettant de prouver cette propriété. Nous donnons
au passage une application des méthodes à la preuve du
théorème de Skolem intuitionniste.
Puis nous étendons le théorème de complétude de
Gödel, en rajoutant la réécriture et en
renforçant l'hypothèse. Cela permet de prouver l'élimination
des coupures pour plusieurs classes de systèmes de
réécriture, à la fois en Déduction
Modulo classique et intuitionniste.
Nous nous intéressons ensuite aux liens existant entre
la propriété d'élimination des coupures et la
propriété de normalisation. À ce titre, nous
fournissons un exemple montrant qu'elles sont distinctes.
Enfin, nous nous intéressons à la
démonstration automatique, et au lien entre la
résolution modulo et le calcul des séquents modulo sans
coupure.
Mots clefs:
Déduction Modulo, coupure, élimination des
coupures, calcul des séquents, résolution, ENAR,
règles de réécriture, sémantique,
modèles booléeens, modèles de Kripke,
complétude, normalisation, Skolem, skolémisation,
logique.
Tous les documents fournis le sont sous la responsabilité de leurs auteurs, et ne représentent pas nécessairement les positions officielles de l'École polytechnique. Les informations données le sont de bonne foi, mais leur véracité ne saurait être garantie.
