{"id":"arxiv/2606.03413","url":"https://arxiv.org/abs/2606.03413","tags":["cs.LO","math.LO"],"score":0,"title":"Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents","domain":"cs.LO","source":"arxiv","authors":["Tim S. Lyon","Lukas Zenger"],"reviews":0,"subject":"cs.LO","summary":"We introduce the formalism of non-wellfounded and cyclic linear nested sequent calculi, developing concrete 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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-06-02","reactions":{}}