LSV Seminar
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.
Past Seminars
Cross-fertilization of proof theory and automated theorem proving : the case of resolution modulo theory
- Date
- Tuesday, November 03 2015 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Guillaume Burel (ENSIIE, Evry)
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.