通过线性化优化 Gödel-Löb 逻辑的树-超矢列证明搜索
Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
AI总结：
针对 GL 逻辑在树-超矢列系统 CSGL 中的可判定性证明和 PSPACE 证明搜索算法问题，提出线性化方法，仅构建单分支推导和树矢列，实现 PSPACE 最优复杂度，并提取有限反模型验证算法正确性。
摘要：
我们回答了 Poggiolesi 提出的关于树-超矢列系统 CSGL 中 GL 的语法可判定性证明的问题，并解决了 Maggesi 和 Perini Brogi 识别的挑战，他们寻求在表达性矢列形式主义中为 GL 寻找 PSPACE 证明搜索算法。我们使用以（标记）树矢列形式表述的 CSGL 的符号变体。我们的答案是复杂度最优的：我们提出了一种证明搜索算法，该算法判定公式的（不）有效性并在 PSPACE 中运行，与已知的 GL 的 PSPACE 完全性相匹配。为实现这一点，我们引入了一种“线性化方法”，该方法每次只构建推导和树矢列的单个分支，避免了在矢列形式主义中朴素证明搜索典型的指数爆炸。我们展示了如何系统地组合证明搜索期间生成的树矢列片段以提取有限反模型，这作为理论工具用于在证明搜索失败时建立算法的正确性。最后，我们证明每个有效公式都有一个仅由线矢列（对应于线性嵌套矢列）组成的证明。这建立了深度优先证明搜索与线性嵌套矢列演算之间的联系。我们的结果不仅回答了上述问题，还为模态逻辑中树矢列系统的证明搜索和正确性论证提供了新见解。
英文摘要：
We answer a question posed by Poggiolesi concerning a syntactic decidability proof for GL in the tree-hypersequent system CSGL, and resolve a challenge identified by Maggesi and Perini Brogi, who sought a PSPACE proof-search algorithm for GL in expressive sequent-based formalisms. We work with a notational variant of CSGL formulated in terms of (labeled) tree sequents. Our answer is complexity-optimal: we present a proof-search algorithm that decides the (in)validity of formulae and runs in PSPACE, matching the known PSPACE-completeness of GL. To achieve this, we introduce a "linearization method", which constructs only a single branch of a derivation and of a tree sequent at a time, avoiding the exponential blowup typical of naive proof-search in sequent formalisms. We show how to systematically combine fragments of tree sequents generated during proof-search to extract finite counter-models, which serves as a theoretical device for establishing the correctness of the algorithm when proof-search fails. Finally, we show that every valid formula admits a proof consisting solely of line sequents, which correspond to linear nested sequents. This establishes a connection between depth-first proof-search and linear nested sequent calculi. Our results not only answer the aforementioned questions, but also provide new insights into proof-search and correctness arguments in tree sequent systems for modal logics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
