The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Deduction modulo theory is a framework in which an existing proof system (e.g. the sequent calculus, the lambda-Pi calculus, or resolution) is enriched with a congruence modulo which the inference rules are applied. It was first introduced to prove the completeness of some automated theorem proving methods. In this talk, we study how proof theory and automated theorem proving both benefit from it. First, the completeness of the combination of two well-known refinements of resolution, namely ordered resolution and set-of-support strategy, is shown to be equivalent to a proof theoretic property, namely the admissibility of the cut rule in the sequent calculus modulo theory. This ensures not only that proving cut admissibility (for instance by proving strong normalization) implies the completeness of resolution modulo theory ; but also that we can use saturation techniques to obtain a presentation of a theory that is suitable for deduction modulo theory. Second, this link can be used to embed resolution modulo theory into an existing automated theorem prover based on resolution, such as iProver. Experiments with iProverModulo show that proof search is indeed improved, in particular for set theories.