Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
2026-06-02 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study special types of logical proofs called non-wellfounded and cyclic linear nested sequents, focusing on their use in linear temporal logic (LTL). They look at two main problems: how to find cycles in these proofs (cycle recognition) and how to turn cyclic proofs back into non-wellfounded ones (unraveling). Their work shows how to recognize cycles using a new property called saturation recurrence, and how to reconstruct non-wellfounded proofs from cyclic ones by moving proof steps along the sequence. This research adds new methods for working with complex proof systems that go beyond traditional logical structures.
non-wellfounded proofscyclic proofslinear nested sequentslinear temporal logiccycle recognitionunravelingsaturation recurrenceGentzen sequentsproof theorymultisequent formalisms
Authors
Tim S. Lyon, Lukas Zenger
Abstract
We introduce and investigate non-wellfounded and cyclic linear nested sequent calculi, and, as a case study, develop such systems for linear temporal logic (LTL). The paper addresses two central problems, which we call 'cycle recognition' and 'unraveling.' Cycle recognition concerns identifying cycles in non-wellfounded proofs in order to extract corresponding cyclic proofs, while unraveling studies the converse transformation, from cyclic proofs to non-wellfounded ones. Although these processes are well understood for Gentzen sequents, they have received little attention for more expressive sequent formalisms and become more challenging in the linear nested sequent setting. To address cycle recognition, we show the completeness of non-wellfounded proofs relative to a particular normal form exhibiting a property we call 'saturation recurrence,' which enables the systematic extraction of cyclic proofs. To address unraveling, we introduce a specialized procedure that shifts rule applications forward along linear nested sequents, allowing non-wellfounded proofs to be reconstructed from cyclic ones. Overall, our work provides new proof-theoretic techniques for cycle recognition and unraveling in expressive multisequent formalisms.