Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Laurent Doyen and Stefan Göller.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Prochain séminaire

Linking Focusing and Resolution with Selection

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Guillaume Burel
Date
Le mardi 26 septembre 2017 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
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.


Séminaires à venir

TBA

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Dietrich Kuske
Date
Le mardi 03 octobre 2017 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Dietrich Kuske (TU Ilmenau)


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 26 septembre
mar. 3 octobre

Les séminaires précédents