Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
Abstract
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.
Versions
Related
- Optimizing Encoder Circuits of Entanglement-Assisted Quantum LDPC Codes via Beam Search
- Optimizing Both Checking and Update Costs in Random Walk Search
- A proof of Ross's conjecture for two-site moving-target search
- The logarithmic spiral is optimal for shoreline search: a computer-assisted proof
- Mechanizing Gödel's Incompleteness Theorems and Provability Logic
BibTeX
@misc{lyon2026optimizing,
title = {{Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents}},
author = {Tim S. Lyon and Omar Y. A. A. Taher},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2606.03484},
eprint = {2606.03484},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2606.03484},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
AU - Tim S. Lyon
AU - Omar Y. A. A. Taher
PY - 2026
DA - 2026/10/11
PB - arXiv
DO - 10.48550/arxiv.2606.03484
UR - https://arxiv.org/abs/2606.03484
AB - 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.
ER -