LTL的非良基与循环证明：与线性嵌套相继式的句法对应
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
AI总结：
本文针对线性时序逻辑（LTL），引入并研究非良基和循环线性嵌套相继式演算，通过饱和递归和规则前移技术，解决了从非良基证明中提取循环证明（循环识别）以及反向转换（展开）两个核心问题。
摘要：
我们引入并研究了非良基和循环线性嵌套相继式演算，并以线性时序逻辑（LTL）为案例开发了此类系统。本文解决了两个核心问题，即“循环识别”和“展开”。循环识别涉及识别非良基证明中的循环，以提取相应的循环证明；而展开研究反向转换，即从循环证明到非良基证明。尽管这些过程在Gentzen相继式中已被充分理解，但对于更具表达力的相继式形式化方法却鲜有关注，并且在线性嵌套相继式设置中变得更加具有挑战性。为了解决循环识别，我们证明了非良基证明相对于一种特定范式的完备性，该范式具有我们称为“饱和递归”的性质，从而能够系统地提取循环证明。为了解决展开，我们引入了一种专门的过程，将规则应用沿线性嵌套相继式向前移动，从而允许从循环证明重构非良基证明。总体而言，我们的工作为表达性多相继式形式化方法中的循环识别和展开提供了新的证明论技术。
英文摘要：
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 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
