12 citations · 68 across the 25 of their papers we have counts for
28 papers
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…
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…
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…
Derivation-Graph-Based Characterizations of Decidable Existential Rule Sets
Tim S. Lyon, Sebastian Rudolph
This paper establishes alternative characterizations of very expressive classes of existential rule sets with decidable query entailment. We consider the notable class of greedy bo…
Nested Sequents for Quantified Modal Logics
Tim S. Lyon, Eugenio Orlandelli
This paper studies nested sequents for quantified modal logics. In particular, it considers extensions of the propositional modal logics definable by the axioms D, T, B, 4, and 5 w…
Connecting Proof Theory and Knowledge Representation: Sequent Calculi and the Chase with Existential Rules
Tim S. Lyon, Piotr Ostropolski-Nalewaja
Chase algorithms are indispensable in the domain of knowledge base querying, which enable the extraction of implicit knowledge from a given database via applications of rules from…
Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics
Tim S. Lyon
We present nested sequent systems for propositional Gödel-Dummett logic and its first-order extensions with non-constant and constant domains, built atop nested calculi for intuiti…
Standpoint Linear Temporal Logic
Nicola Gigante, Lucia {Gomez Alvarez}, Tim S. Lyon
Many complex scenarios require the coordination of agents possessing unique points of view and distinct semantic commitments. In response, standpoint logic (SL) was introduced in t…
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…
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…
Nested Sequents for First-Order Modal Logics via Reachability Rules
Tim S. Lyon
We introduce the first cut-free nested sequent systems for first-order modal logics that admit increasing, decreasing, constant, and empty domains along with so-called general path…
Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying
Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja +1
In our pursuit of generic criteria for decidable ontology-based querying, we introduce 'finite-cliquewidth sets' (FCS) of existential rules, a model-theoretically defined class of…
A logical analysis of instrumentality judgments: means-end relations in the context of experience and expectations
Kees van Berkel, Tim S. Lyon, Matteo Pascucci
This article proposes the use of temporal logic for an analysis of instrumentality inspired by the work of G.H. von Wright. The first part of the article contains the philosophical…
Uniform and Modular Sequent Systems for Description Logics
Tim Lyon, Jonas Karge
We introduce a framework that allows for the construction of sequent systems for expressive description logics extending ALC. Our framework not only covers a wide array of common d…
Automating Reasoning with Standpoint Logic via Nested Sequents
Tim S. Lyon, Lucía Gómez Álvarez
Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of div…
A Framework for Intuitionistic Grammar Logics
Tim S. Lyon
We generalize intuitionistic tense logics to the multi-modal case by placing grammar logics on an intuitionistic footing. We provide axiomatizations for a class of base intuitionis…
Refining Labelled Systems for Modal and Constructive Logics with Applications
Tim Lyon
This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economi…
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
Tim S. Lyon
We employ a recently developed methodology -- called "structural refinement" -- to extract nested sequent systems for a sizable class of intuitionistic modal logics from their resp…
On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
Tim Lyon
This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first…
Display to Labeled Proofs and Back Again for Tense Logics
Agata Ciabattoni, Tim S. Lyon, Revantha Ramanayake +1
We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus f…
Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents
Tim Lyon
This paper employs the linear nested sequent framework to design a new cut-free calculus LNIF for intuitionistic fuzzy logic--the first-order Gödel logic characterized by linear re…
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
Tim Lyon
This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecti…
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
Tim Lyon, Alwen Tiu, Rajeev Goré +1
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this met…