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.

翻译：我们引入并研究了非良基与循环线性嵌套相继式演算，并以线性时序逻辑（LTL）为例开发了此类系统。本文解决了两个核心问题，即“循环识别”与“展开化”。循环识别关注于在非良基证明中识别循环，以提取对应的循环证明；而展开化则研究从循环证明到非良基证明的逆变换。尽管这些过程在Gentzen相继式中已得到充分理解，但对于更具表达力的相继式形式化而言，它们鲜受关注，且在线性嵌套相继式背景下变得更具挑战性。针对循环识别，我们证明了非良基证明相对于一种称为“饱和递归”性质的特定范式的完备性，从而实现了循环证明的系统性提取。针对展开化，我们引入了一种专用程序，该程序将规则应用沿线性嵌套相继式前移，使得能够从循环证明重构非良基证明。总体而言，我们的工作为具有表达力的多相继式形式化中的循环识别与展开化提供了新的证明论技术。