# 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

### Linking Focusing and Resolution with Selection

- Date
- Tuesday, September 26 2017 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Guillaume Burel (ENSIIE, Evry)

In automated theorem proving, general methods such as resolution or
sequent calculi need to be restricted in practice to reduce the proof
search space. For resolution-based methods, the main approach to do so
consists in restraining which literals can be resolved upon in a given
clause. This has lead e.g. to ordered resolution with
selection. Independently, focusing was introduced in sequent calculi
to get a better control of the applications of the inference rules.
We relate these two techniques by generalizing them: We introduce a
sequent calculus where each occurrence of an atom can have a positive
or a negative polarity (in the focusing sense); and a resolution
method where each literal, whatever its sign, can be selected. We
prove the equivalence between cut-free proofs in this sequent calculus
and derivations of the empty clause in that resolution method.

We therefore obtain a family of related proof methods. They are in
general not complete, which allow us to use theoretically strong
completeness proofs for some particular instances. We present three of
these complete instances: first, our framework allows us to show that
ordinary focusing corresponds to hyperresolution and semantic resolution;
the second instance is deduction modulo theory; and a new setting
extends deduction modulo theory with rewriting rules having several
left-hand sides, therefore restricting even more the proof search
space.