{"id":"arxiv/2606.03484","url":"https://arxiv.org/abs/2606.03484","tags":["cs.LO","math.LO"],"score":0,"title":"Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents","domain":"cs.LO","source":"arxiv","authors":["Tim S. Lyon","Omar Y. A. A. Taher"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-06-02","reactions":{}}