7 papers
Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations
Tim S. Lyon
We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb provability logic. In particular, we consider Sambin and Vale…
Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
Tim S. Lyon, Omar Taher
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 Pe…
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
Tim S. Lyon, Lukas Zenger
We introduce and investigate non-wellfounded and cyclic linear nested sequent calculi, and, as a case study, develop such systems for linear temporal logic (LTL). The paper address…
Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
Tim S. Lyon, Eugenio Orlandelli
We introduce cut-free nested sequent systems for a broad class of quantified modal logics (QMLs). The QMLs we consider are semantically defined using relational models that assign…
Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents
Tim S. Lyon
This paper develops a novel nested sequent proof-search methodology for intuitionistic tense logics (ITLs), supporting finite counter-model extraction. We introduce a new loop-chec…
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
Tim S. Lyon, Agata Ciabattoni, Didier Galmiche +5
This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuiti…