Advisor:
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
Abstract:
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.
Keywords:
Deduction Modulo, cut, cut elimination, sequent calculus,
resolution, ENAR, rewriting rules, semantics, boolean models, Kripke
models, completeness, normalization, Skolem, skolemization, logic.
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.
