{
  "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.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": "Journal reference: EPTCS 454, 2026, pp. 148-164",
  "arxiv": "2606.03484",
  "author_total": 2,
  "authors": [
    {
      "name": "Tim S. Lyon"
    },
    {
      "name": "Omar Y. A. A. Taher"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/1kgpdabx54rz8.bib",
  "cited_by": 0,
  "doi": "10.48550/arxiv.2606.03484",
  "fulltext_url": null,
  "id": "1kgpdabx54rz8",
  "issns": [],
  "landing_url": "https://arxiv.org/abs/2606.03484",
  "language": null,
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "http://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": "CC0-1.0",
  "native_subjects": [
    [
      "arxiv",
      "cs.LO"
    ],
    [
      "arxiv",
      "math.LO"
    ]
  ],
  "openalex": null,
  "pdf_url": "https://arxiv.org/pdf/2606.03484",
  "pmcid": null,
  "pmid": null,
  "published": "2026-10-11",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/1kgpdabx54rz8.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:29:15Z",
      "native_id": "2606.03484",
      "source": "arxiv",
      "url": "https://arxiv.org/abs/2606.03484"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "arxiv:math.LO",
      "subfield": "logic-foundations"
    }
  ],
  "title": "Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents",
  "title_text": "Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents",
  "type": "preprint",
  "updated_at": "2026-10-30T12:29:15Z",
  "url": "https://research.draconitic.com/paper/1kgpdabx54rz8",
  "venue": "arXiv",
  "versions": [
    {
      "doi": "10.4204/eptcs.454.11",
      "pid": null,
      "relation": "published-as",
      "title": null,
      "venue": null
    }
  ]
}