University of Birmingham > Talks@bham > Theoretical computer science seminar > Cyclic Proofs, Hypersequents, and Transitive Closure Logic

Cyclic Proofs, Hypersequents, and Transitive Closure Logic

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Tom de Jong.

Zoom details


Transitive Closure Logic (TCL) enriches the language of first order logic with a recursive operator, expressing the transitive closure of a binary relation. Cyclic sequent calculi proofs for this logic have been introduced in the literature. In this talk, I will present a new cyclic proof system for TCL , which employs hypersequents. The main motivation behind this work is that, differently from sequent TCL proofs, hypersequent proofs for TCL successfully simulate cyclic proofs in the transitive fragment of Propositional Dynamic Logic (PDL+), without using the non-analytic rule of cut. After introducing the cyclic hypersequent calculus for TCL , I will present two main results. First, I will sketch a proof of soundness for the calculus, which requires a more involved argument than the one used in traditional cyclic proofs. Second, I will show how PDL + cyclic proofs can be translated into TCL hypersequent proofs. This result allows to lift the completeness result for cyclic Propositional Dynamic Logic to the hypersequent calculus.

This talk is based on joint work with Anupam Das.

Sonia Marin has kindly agreed to chair this talk.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.