12 papers
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…
On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
Tim S. Lyon
Propositional dynamic logic (PDL) is an important modal logic used to specify and reason about the behavior of software. A challenging problem in the context of PDL is solving fixe…
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 Valent…
Realizing the Maximal Analytic Display Fragment of Labeled Sequent Calculi for Tense Logics
Tim S. Lyon
We define and study translations between the maximal class of analytic display calculi for tense logics and labeled sequent calculi, thus solving an open problem about the translat…
Decidability of Quasi-Dense Modal Logics
Piotr Ostropolski-Nalewaja, Tim S. Lyon
The decidability of axiomatic extensions of the modal logic K with modal reduction principles, i.e. axioms of the form , has remained a l…
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
Tim S. Lyon, Ian Shillito, Alwen Tiu
It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of…
Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
Tim S. Lyon, Jonas Karge
We introduce a constructive method applicable to a large number of description logics (DLs) for establishing the concept-based Beth definability property (CBP) based on sequent sys…
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…