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.