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 Laurent Doyen and Stefan Göller.

The seminar is open to public and does not require any form of registration.

Next Seminar

Linking Focusing and Resolution with Selection

Visit website for this news | Export event in iCalendar format

 Guillaume Burel
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.


Upcoming Seminars

TBA

Visit website for this news | Export event in iCalendar format

 Dietrich Kuske
Date
Tuesday, October 03 2017 at 11:00AM
Place
Salle de Conférence (Pavillon des Jardins)
Speaker
Dietrich Kuske (TU Ilmenau)


About LSV

Agenda

Export agenda in iCalendar format | Past seminars

Tue, Sep 26
Tue, Oct 3

Past seminars