BEGIN:VCALENDAR
VERSION:2.0
PRODID:talks.ox.ac.uk
BEGIN:VEVENT
SUMMARY:Axioms as rules: How to reason with mathematical theories - Prof.
Elaine Pimentel (University College London)
DTSTART;VALUE=DATE-TIME:20231128T150000Z
DTEND;VALUE=DATE-TIME:20231128T160000Z
UID:https://new.talks.ox.ac.uk/talks/id/58e794a9-cb72-443b-9d1b-7636abe42f
94/
DESCRIPTION:One of the advantages of using sequent systems as a framework
for logical reasoning is that the resulting calculi are often simple\, hav
e good proof theoretical properties (like cut-elimination\, consistency\,
etc) and can be easily implemented\, eg using rewriting.\n\nHence it would
be heaven if we could add axioms in mathematical theories to first order
logics and reason about them using all the machinery already built for the
sequent framework. Indeed\, the general problem of extending standard pro
of-theoretical results obtained for pure logic to certain classes of non-l
ogical axioms has been the focus of attention for quite some time now.\n\n
The main obstacle for this agenda is that adding non-logical axioms to sys
tems while still maintaining the good proof theoretical properties is not
an easy task. In fact\, adding naively axioms to sequent systems often res
ult in non cut-free systems. One way of circumventing this problem is by t
reating axioms as theories\, added to the sequent context. This is already
in Gentzen's consistency proof of elementary arithmetic. Now the derivati
ons have only logical axioms as premises\, and cut elimination applies.\n\
nBut we can do better by transforming axioms into inference rules. In this
talk\, we will propose a systematic way of adding inference rules to sequ
ent systems. The proposal will be based on the notions of focusing and pol
arities. We will also discuss how our framework escalates to hypersequents
and systems of rules\, and the application of this to modal logics\, proo
fs explanation and SMT solvers.\n\nThis is a joint work with Dale Miller\,
Sonia Marin\, Marco Volpe\, Francesca Poggiolesi and Yoni Zohar.\nSpeaker
s:\nProf. Elaine Pimentel (University College London)
LOCATION:Wolfson Building (LTB)\, Parks Road OX1 3QD
TZID:Europe/London
URL:https://new.talks.ox.ac.uk/talks/id/58e794a9-cb72-443b-9d1b-7636abe42f
94/
BEGIN:VALARM
ACTION:display
DESCRIPTION:Talk:Axioms as rules: How to reason with mathematical theories
- Prof. Elaine Pimentel (University College London)
TRIGGER:-PT1H
END:VALARM
END:VEVENT
END:VCALENDAR