6 papers · 1 filter
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…