Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents

Tim LyonTim Lyon, Omar TaherOmar Taher

Tim Lyon, Omar Taher
Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
In Giorgio Bacci and Mickaël Randour, eds., Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2026), volume 454, 148-164, 2026. Electronic Proceedings in Theoretical Computer Science

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{LT2026,
  author    = {Tim Lyon and Omar Taher},
  title     = {Optimizing Proof-Search via Linearization for
               G{\"{o}}del-L{\"{o}}b Logic with Tree-Hypersequents},
  editor    = {Giorgio Bacci and Micka{\"{e}}l Randour},
  booktitle = {Proceedings Seventeenth International Symposium on Games,
               Automata, Logics, and Formal Verification (GandALF 2026)},
  volume    = {454},
  publisher = {Electronic Proceedings in Theoretical Computer Science},
  year      = {2026},
  pages     = {148-164}
}