# 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.