Tim S. Lyon

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

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...

Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents

We introduce the formalism of non-wellfounded and cyclic linear nested sequent calculi, developing concrete systems for linear temporal logic (LTL). The paper addresses two central problems, which we call "cycle recognition" and "unraveling." Cycle recognition concerns identifyin...