  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.
