Decidability of Quasi-Dense Modal Logics

TL;DR

This work addresses the long-standing open problem of the decidability of quasi-dense modal logics, i.e., normal modal extensions of $\mathsf{K}$ by axioms of the form $\Diamond^k p \rightarrow \Diamond^n p$ with $0 < k < n$. It introduces a novel synthesis of modal reasoning with database-style reasoning via disjunctive existential rules and encodes each modal formula $\varphi$ as a first-order database $\mathcal{D}_{\varphi}$ plus a rule set $\mathcal{R}_{\varphi} \cup \mathcal{P}$, where $\mathcal{P}$ encodes quasi-density properties. The key technical advance is a model-theoretic argument that chase-generated models can be finitely encoded as templates, obtained through unfold/trim/core operations, which bounds the search space and yields an $\textsc{EXPSPACE}$ decision procedure. Consequently, every quasi-dense logic $\mathsf{L}(\mathcal{P})$ is decidable, advancing toward a full resolution of modal reduction logic decidability and opening new avenues for applying database-theoretic methods to modal satisfiability problems.

Abstract

The decidability of axiomatic extensions of the modal logic K with modal reduction principles, i.e. axioms of the form $\Diamond^{k} p \rightarrow \Diamond^{n} p$, has remained a long-standing open problem. In this paper, we make significant progress toward solving this problem and show that decidability holds for a large subclass of these logics, namely, for 'quasi-dense logics.' Such logics are extensions of K with with modal reduction axioms such that $0 < k < n$ (dubbed 'quasi-density axioms'). To prove decidability, we define novel proof systems for quasi-dense logics consisting of disjunctive existential rules, which are first-order formulae typically used to specify ontologies in the context of database theory. We show that such proof systems can be used to generate proofs and models of modal formulae, and provide an intricate model-theoretic argument showing that such generated models can be encoded as finite objects called 'templates.' By enumerating templates of bound size, we obtain an EXPSPACE decision procedure as a consequence.

Figures (3)

• Figure 1: Example unfolding of a rooted DAG $\mathcal{I}$. The dashed blue edges are $E$, while solid gray edges are $R$. Note how terms in the unfolded instance are uniquely identified by paths from the root of $\mathcal{I}$.
• Figure 2: Example trimming of a multi-tree to the depth of two. The dashed blue edges are $E$, while solid gray edges are $R$. Note how $E$ paths are preserved if they start below depth of three.
• Figure 3: Two embeddings along with their unravelings where dash-dotted lines represent partial isomorphisms. The left embedding is improper as witnessed by an additional outgoing $E$-atom of $t_+$. The right embedding is proper, as witnessed by its unraveling being isomorphic to $\mathcal{S}$. Note that in both cases $t_+$ and $s_+$ are deeper then the counterparts $t'$ and $s'$, and thus the sub-trees of $tbct'$ and $sbcs'$ are only partially isomorphic to the respective sub-trees $tat'$ and $sas'$.

Theorems & Definitions (22)

• Definition 1: $\mathcal{P}$-Model
• Definition 2: Semantic Clauses
• Theorem 3
• Definition 5
• Definition 6
• Lemma 7
• Theorem 8: Soundness
• Theorem 9: Completeness
• Lemma 12
• Definition 13: $\mathsf{unfold}$