5 papers · 2 filters
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
Tim S. Lyon, Lukas Zenger
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…
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
Tim S. Lyon, Lukas Zenger
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…
Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
Tim S. Lyon, Omar Taher, Omar Y. A. A. 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…
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…