BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
Linking Focusing and Resolution with Selection
STATUS:CONFIRMED
ATTENDEE;CN="Guillaume Burel
":
MAILTO:no@spam.com
DESCRIPTION:
In automated theorem proving\, general methods such as resol
ution or sequent calculi need to be restricted in practice t
o reduce the proof search space. For resolution-based method
s\, the main approach to do so consists in restraining which
literals can be resolved upon in a given clause. This has l
ead e.g. to ordered resolution with selection. Independently
\, focusing was introduced in sequent calculi to get a bette
r control of the applications of the inference rules. We rel
ate 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 si
gn\, can be selected. We prove the equivalence between cut-f
ree proofs in this sequent calculus and derivations of the e
mpty clause in that resolution method. We therefore obtain a
family of related proof methods. They are in general not co
mplete\, which allow us to use theoretically strong complete
ness proofs for some particular instances. We present three
of these complete instances: first\, our framework allows us
to show that ordinary focusing corresponds to hyperresoluti
on and semantic resolution; the second instance is deduction
modulo theory; and a new setting extends deduction modulo t
heory with rewriting rules having several left-hand sides\,
therefore restricting even more the proof search space.
DTSTART;TZID=Europe/Paris:20170926T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201709261
100
UID:LSVsemLSV.201709261100@lsv.ens-cachan.fr
LOCATION:Salle de ConfĂ©rence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR