一句话：证明准稠密模态逻辑可判定，并给出基于模板枚举的 ExpSpace 判定过程。
对模态逻辑 K 的公理扩张，若加入形如 ⋄^k p → ⋄^n p 的模态归约原则，其可判定性长期悬而未决。本文针对其中满足 0 < k < n 的准稠密逻辑取得进展，证明该大类可判定。作者为这类逻辑定义由析取存在规则组成的新型证明系统；这些规则通常用于数据库理论中的本体规格。作者表明该系统既能生成模态公式的证明，也能生成其模型，并借助精细的模型论论证，将生成的模型编码为有限对象——模板。通过枚举有界大小的模板，论文得到一个 ExpSpace 判定程序，从而证明准稠密模态逻辑的可判定性。
The decidability of axiomatic extensions of the modal logic K with modal reduction principles, i.e. axioms of the form ⋄kp → ⋄np, 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 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.