Title: Cyclic Proofs with Nested Sequents

Speaker: Lukas Zenger (Peking University)

Time: Sep. 15th (Tuesday) 15:10 - 18:00

Location: Teaching Building No.2 (二教) 411

Abstract:

Modal fixed-point and program logics extend modal languages with operators for expressing inductive and coinductive definitions. Due to these constructs, such logics often require reasoning principles that go beyond finite, well-founded proofs. One approach to obtain cut-free and analytic proof systems for such logics is to employ non-wellfounded proofs, which take the form of non-wellfounded trees and rely on global correctness conditions to ensure soundness. Such proofs can be viewed as a formalization of reasoning by infinite descent. When non-wellfounded proofs have the shape of a regular tree - containing only finitely many distinct subtrees - they can be folded into finite proofs in which certain leaves are linked back to internal nodes, thereby creating cycles. This gives rise to cyclic proofs, which provide a finite representation of non-wellfounded proofs and are amenable to automated proof-search and to computing interpolants. An important question in non-wellfounded proof theory is how to transform non-wellfounded proofs into cyclic proofs and, conversely, how to unravel cyclic proofs into non-wellfounded ones. While such transformations are well understood for proof systems based on ordinary sequents, the problem remains largely open for systems employing richer structures, such as labeled or nested sequents. In this talk, we discuss the challenges that arise in the nested-sequent setting and present a solution for a non-wellfounded proof system for LTL based on linear nested sequents.