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.

翻译：模态逻辑K的模态归约原则（即形式为$\Diamond^{k} p \rightarrow \Diamond^{n} p$的公理）的公理化扩张的可判定性一直是一个长期悬而未决的问题。本文在解决该问题上取得了重要进展，证明了这类逻辑中一个广泛子类——即"拟稠逻辑"——的可判定性成立。此类逻辑是在K中添加满足$0 < k < n$的模态归约公理（称为"拟稠性公理"）的扩张。为证明可判定性，我们为拟稠逻辑定义了由析取存在规则构成的新型证明系统，这类规则是数据库理论中通常用于描述本体的一阶公式。我们证明此类证明系统可用于生成模态公式的证明与模型，并通过精巧的模型论论证表明：所生成的模型可编码为称为"模板"的有限对象。通过枚举有界尺寸的模板，我们最终得到一个EXPSPACE下的判定算法。