BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Cut-elimination\, Cut-restriction - Timo Lang (UCL
)
DTSTART:20231027T100000Z
DTEND:20231027T105000Z
UID:TALK5352AT
URL:/talk/index/5352
DESCRIPTION:*Zoom details*\n\n* Link: https://bham-ac-uk.zoom.
us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IU
T09\n* Meeting ID: 818 7333 5084\n* Passcode: 217\
n\n*Abstract*\n\nIn the 1930s\, Gerhard Gentzen in
itiated the field of structural proof theory with
his celebrated cut-elimination theorem. For this\,
he invented a formal system for the notation of m
athematical proofs called the sequent calculus\, a
nd then showed that\, in this calculus\, applicati
ons of the cut rule—roughly corresponding to the u
se of lemmas in proofs—can always be eliminated.\n
\nOriginally developed for classical and intuition
istic logic\, Gentzen’s method has since been succ
essfully applied to a large variety of nonclassica
l logics. Yet\, there are some logics\, such as th
e modal logic S5\, where the method—at least in it
s original form—cannot be applied. The standard so
lution to this problem involves seeking structural
extensions of the sequent calculus in which cut-e
limination goes through. This program has been ver
y successful and has given rise to many formalisms
such as the hypersequent calculus and the nested
sequent calculus. The price to pay is that proofs
in these structural extensions can be quite comple
x even after cuts are removed.\n\nIn this talk\, I
discuss joint work with Agata Ciabattoni (TU Wien
) and Revantha Ramanayake (RU Groningen) that deal
s with an alternative approach: Instead of pursuin
g cut-elimination in extensions of the sequent cal
culus\, we retain the sequent calculus and examine
which cuts are necessary to capture a logic. Whil
e there are some scattered results on this approac
h in the literature\, it has been overshadowed by
cut-elimination. As it turns out\, sometimes the f
ormat of necessary cuts is quite simple and doesn’
t really hamper the analysis of proofs. Beyond suc
h practical considerations\, we think that the stu
dy of such 'cut-restriction' results offers a valu
able complementary outlook compared to the extensi
on-focused view.
LOCATION:LG23\, Computer Science // Zoom
CONTACT:George Kaye
END:VEVENT
END:VCALENDAR