arXiv subjects

Tim S. Lyon

Publications and source records attributed to Tim S. Lyon.

29 records · Page 2Linked to original sources

arXiv2023

Nested Sequents for First-Order Modal Logics via Reachability Rules

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 conditions and seriality. We obtain such systems by means of two devices: 'reachability rules' and 'structural refinement'. Regarding the former device, we introduce reachability rules as special logical rules parameterized with formal grammars (viz. types of semi-Thue systems) that operate by propagating formulae and/or checking if data exists along certain paths within a nested sequent, where paths are encoded as strings generated by a parameterizing grammar. Regarding the latter device, structural refinement is a relatively new methodology used to extract nested sequent systems from labeled systems (which are ultimately obtained from a semantics) by means of eliminating structural/relational rules, introducing reachability rules, and then carrying out a notational translation. We therefore demonstrate how this method can be extended to the setting of first-order modal logics, and expose how reachability rules naturally arise from applying this method.

cs.LO↗

arXiv2023

Nested Sequents for Quantified Modal Logics

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 with varying, increasing, decreasing, and constant domains. Each calculus is proved to have good structural properties: weakening and contraction are height-preserving admissible and cut is (syntactically) admissible. Each calculus is shown to be equivalent to the corresponding axiomatic system and, thus, to be sound and complete. Finally, it is argued that the calculi are internal -- i.e., each sequent has a formula interpretation -- whenever the existence predicate is expressible in the language.

math.LO↗

arXiv2023

Derivation-Graph-Based Characterizations of Decidable Existential Rule Sets

This paper establishes alternative characterizations of very expressive classes of existential rule sets with decidable query entailment. We consider the notable class of greedy bounded-treewidth sets (gbts) and a new, generalized variant, called weakly gbts (wgbts). Revisiting and building on the notion of derivation graphs, we define (weakly) cycle-free derivation graph sets ((w)cdgs) and employ elaborate proof-theoretic arguments to obtain that gbts and cdgs coincide, as do wgbts and wcdgs. These novel characterizations advance our analytic proof-theoretic understanding of existential rules and will likely be instrumental in practice.

cs.LO↗

arXiv2023

Connecting Proof Theory and Knowledge Representation: Sequent Calculi and the Chase with Existential Rules

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 a given ontology. Such algorithms have proved beneficial in identifying logical languages which admit decidable query entailment. Within the discipline of proof theory, sequent calculi have been used to write and design proof-search algorithms to identify decidable classes of logics. In this paper, we show that the chase mechanism in the context of existential rules is in essence the same as proof-search in an extension of Gentzen's sequent calculus for first-order logic. Moreover, we show that proof-search generates universal models of knowledge bases, a feature also exhibited by the chase. Thus, we formally connect a central tool for establishing decidability proof-theoretically with a central decidability tool in the context of knowledge representation.

cs.LO↗

arXiv2023

Standpoint Linear Temporal Logic

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 the context of knowledge integration, allowing one to reason with diverse and potentially conflicting viewpoints by means of indexed modalities. Another multi-modal logic of import is linear temporal logic (LTL) - a formalism used to express temporal properties of systems and processes, having prominence in formal methods and fields related to artificial intelligence. In this paper, we present standpoint linear temporal logic (SLTL), a new logic that combines the temporal features of LTL with the multi-perspective modelling capacity of SL. We define the logic SLTL, its syntax, and its semantics, establish its decidability and complexity, and provide a terminating tableau calculus to automate SLTL reasoning. Conveniently, this offers a clear path to extend existing LTL reasoners with practical reasoning support for temporal reasoning in multi-perspective settings.

cs.AI↗

arXiv2023

A logical analysis of instrumentality judgments: means-end relations in the context of experience and expectations

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 foundations. We discuss von Wright's general theory of agency and his account of instrumentality. Moreover, we propose several refinements to this framework via rigorous definitions of the core notions involved. In the second part, we develop a logical system called Temporal Logic of Action and Expectations (TLAE). The logic is inspired by a fragment of propositional dynamic logic based on indeterministic time. The system is proven to be weakly complete relative to its given semantics. We then employ TLAE to formalise and analyse the instrumentality relations defined in the first part of the paper. Last, we point out philosophical implications and possible extensions of our work.

math.LO↗

arXiv2022

Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying

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 rule sets, inspired by the cliquewidth measure from graph theory. By a generic argument, we show that FCS ensures decidability of entailment for a sizable class of queries (dubbed 'DaMSOQs') subsuming conjunctive queries (CQs). The FCS class properly generalizes the class of finite-expansion sets (FES), and for signatures of arity at most 2, the class of bounded-treewidth sets (BTS). For higher arities, BTS is only indirectly subsumed by FCS by means of reification. Despite the generality of FCS, we provide a rule set with decidable CQ entailment (by virtue of first-order-rewritability) that falls outside FCS, thus demonstrating the incomparability of FCS and the class of finite-unification sets (FUS). In spite of this, we show that if we restrict ourselves to single-headed rule sets over signatures of arity at most 2, then FCS subsumes FUS.

cs.LO↗

arXiv2022

Automating Reasoning with Standpoint Logic via Nested Sequents

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 diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics--proof systems that manipulate trees whose nodes are multisets of formulae--and show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms. To obtain worst-case complexity-optimal proof-search, we introduce a novel technique in the context of nested sequents, referred to as "coloring," which consists of taking a formula as input, guessing a certain coloring of its subformulae, and then running proof-search in a nested sequent calculus on the colored input. Our technique lets us decide the validity of standpoint formulae in CoNP since proof-search only produces a partial proof relative to each permitted coloring of the input. We show how all partial proofs can be fused together to construct a complete proof when the input is valid, and how certain partial proofs can be transformed into a counter-model when the input is invalid. These "certificates" (i.e. proofs and counter-models) serve as explanations of the (in)validity of the input.

cs.LO↗

arXiv2021

A Framework for Intuitionistic Grammar Logics

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 intuitionistic grammar logics as well as provide axiomatizations for extensions with combinations of seriality axioms and what we call "intuitionistic path axioms". We show that each axiomatization is sound and complete with completeness being shown via a typical canonical model construction.

math.LO↗

arXiv2021

Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

We employ a recently developed methodology -- called "structural refinement" -- to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are parameterized with formal grammars, and which encode certain frame conditions expressible as first-order Horn formulae that correspond to a subclass of the Scott-Lemmon axioms. We show that our nested systems are sound, cut-free complete, and admit hp-admissibility of typical structural rules.

cs.LO↗

arXiv2021

Display to Labeled Proofs and Back Again for Tense Logics

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 for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics.

cs.LO↗