Méthodes sémantiques en Déduction Modulo

Pr. Gilles Dowek

Examining Committee:
Pr. Thierry Coquand (referee)
Pr. Mitsuhiro Okada (referee)
Pr. Jean Goubault-Larrecq
Pr. Thérèse Hardin (president)
Pr. Delia Kesner
Pr. James Lipton

Defended the 6th of December, 2005

Deduction Modulo is a logical frame allowing to integrate deduction and computation via rewrite rules. This way we obtain more modular logical framworks, thanks to the wide range of potential rewrite rules, more readable proofs, a system adapted to automatic theorem proving, an we can also express axiomatic theories with the only mean of rewrite rules.
This work is mainly focused on the property of cut elimination of Deduction Modulo. This is a key property, since it implies consistency of the calculus, and allows to have efficient proof search algorithms. In deduction modulo, this property is not always true.
This PhD thesis first introduces the semantical tools we will use to prove the property. We then give an application to the proof of Skolem theorem in an intuitionnistic frame.
In a second part, we extend Gödel's completeness theorem, strengthening it and extending it with rewrite rules. We get the cut elimination property for a wide range of rewrite systems. This work is done in both classical and intuitionistic Deduction Modulo.
We also focus on the link between our method and the proof normalization method. We give an example proving that both methods are distinct.
In a last part, we focus on the resolution modulo method and its link with the cut-free fragment of sequent calculus modulo.

Deduction Modulo, cut, cut elimination, sequent calculus, resolution, ENAR, rewriting rules, semantics, boolean models, Kripke models, completeness, normalization, Skolem, skolemization, logic.

URL originale de cette page: http://www.lix.polytechnique.fr/~hermant/these_eng.html
Modifiée pour la dernière fois le: 16/02/2006
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.