6 papers
Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability
Tim S. Lyon
We introduce and study single-conclusioned nested sequent calculi for a broad class of intuitionistic multi-modal logics known as "intuitionistic grammar logics (IGLs)." These logi…
The Varieties of Ought-Implies-Can and Deontic STIT Logic
Kees van Berkel, Tim S. Lyon
STIT logic is a prominent framework for the analysis of multi-agent choice-making. In the available deontic extensions of STIT, the principle of Ought-implies-Can (OiC) fulfills a…
Foundations for an Abstract Proof Theory in the Context of Horn Rules
Tim S. Lyon, Piotr Ostropolski-Nalewaja
We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that…
Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement
Tim S. Lyon
Intuitionistic grammar logics fuse constructive and multi-modal reasoning while permitting the use of converse modalities, serving as a generalization of standard intuitionistic mo…
Decidability of Querying First-Order Theories via Countermodels of Finite Width
Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja +1
We propose a generic framework for establishing the decidability of a wide range of logical entailment problems (briefly called querying), based on the existence of countermodels t…
Proof Theory and Decision Procedures for Deontic STIT Logics
Tim S. Lyon, Kees van Berkel
This paper provides a set of cut-free complete sequent-style calculi for deontic STIT ('See To It That') logics used to formally reason about choice-making, obligations, and norms…