BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Cyclic Proofs\, Hypersequents\, and Transitive Clo
sure Logic - Marianna Girlando (University of Birm
ingham)
DTSTART:20220225T140000Z
DTEND:20220225T150000Z
UID:TALK4837AT
URL:/talk/index/4837
DESCRIPTION:**Zoom details**\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\nTransitive Closure Logic (TCL) e
nriches the language of first order logic with a r
ecursive operator\, expressing the transitive clos
ure of a binary relation. Cyclic sequent calculi p
roofs for this logic have been introduced in the l
iterature. In this talk\, I will present a new cyc
lic proof system for TCL\, which employs hypersequ
ents. The main motivation behind this work is that
\, differently from sequent TCL proofs\, hypersequ
ent proofs for TCL successfully simulate cyclic pr
oofs in the transitive fragment of Propositional D
ynamic Logic (PDL+)\, without using the non-analyt
ic rule of cut. After introducing the cyclic hyper
sequent calculus for TCL\, I will present two main
results. First\, I will sketch a proof of soundne
ss for the calculus\, which requires a more involv
ed argument than the one used in traditional cycli
c proofs. Second\, I will show how PDL+ cyclic pro
ofs can be translated into TCL hypersequent proofs
. This result allows to lift the completeness resu
lt for cyclic Propositional Dynamic Logic to the h
ypersequent calculus.\n\nThis talk is based on joi
nt work with Anupam Das.\n\nSonia Marin has kindly
agreed to chair this talk.
LOCATION:LG23\, SoCS and Zoom (see abstract for link)
CONTACT:Tom de Jong
END:VEVENT
END:VCALENDAR