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.

翻译：我们回答了Poggiolesi提出的关于树超矢量系统CSGL中GL的语法可判定性证明的问题,并解决了Maggesi与Perini Brogi发现的挑战,他们寻求在表达性基于矢量的形式体系中为GL寻找PSPACE证明搜索算法。我们使用以(带标记的)树矢量为形式表述的CSGL的记法变体。我们的答案在复杂度上是最优的:我们提出了一种证明搜索算法,该算法判定公式的(非)有效性,并在PSPACE中运行,匹配了已知的GL的PSPACE完全性。为此,我们引入了"线性化方法",该方法每次仅构造推导和树矢量的单个分支,避免了朴素证明搜索在矢量形式体系中典型的指数级膨胀。我们展示了如何系统地组合在证明搜索过程中生成的树矢量片段,以提取有限反模型,这作为理论工具,用于在证明搜索失败时确立算法的正确性。最后,我们证明每个有效公式都允许一个仅由线矢量(对应于线性嵌套矢量)构成的证明。这建立了深度优先证明搜索与线性嵌套矢量演算之间的联系。我们的结果不仅回答了前述问题,还为模态逻辑树矢量系统中的证明搜索与正确性论证提供了新见解。