Decidability of Quasi-Dense Modal Logics

TL;DR

This paper proves that a broad class of quasi-dense modal logics, extending K with specific reduction axioms, are decidable by developing novel proof systems and model-encoding techniques.

Contribution

It introduces new proof systems based on disjunctive existential rules for quasi-dense logics and demonstrates their decidability via finite model encoding.

Findings

Decidability established for quasi-dense modal logics.

Development of novel proof systems using disjunctive existential rules.

An EXPSPACE decision procedure for these logics.

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.