We first consider two decidable fragments of quantified modal logic $\mathsf{S5}$: the one-variable fragment $\mathsf{Q}^1\mathsf{S5}$ and its extension $\mathsf{S5}_{\mathcal{ALC}^u}$ that combines $\mathsf{S5}$ and the description logic $\mathcal{ALC}$ with the universal role. As neither of them enjoys Craig interpolation or projective Beth definability, the existence of interpolants and explicit definitions of predicates -- which is crucial in many knowledge engineering tasks -- does not directly reduce to entailment. Our concern therefore is the computational complexity of deciding whether (uniform) interpolants and definitions exist for given input formulas, signatures and ontologies. We prove that interpolant and definition existence in $\mathsf{Q}^1\mathsf{S5}$ and $\mathsf{S5}_{\mathcal{ALC}^u}$ is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. Then we show that interpolant and definition existence in the one-variable fragment $\mathsf{Q}^1\mathsf{K}$ of quantified modal logic $\mathsf{K}$ is nonelementary decidable, while uniform interpolant existence is undecidable.

翻译：我们首先考虑量化模态逻辑$\mathsf{S5}$的两个可判定片段：单变量片段$\mathsf{Q}^1\mathsf{S5}$及其扩展$\mathsf{S5}_{\mathcal{ALC}^u}$，后者将$\mathsf{S5}$与包含全域角色的描述逻辑$\mathcal{ALC}$相结合。由于这两个片段均不具备Craig插值性或投影Beth可定义性，插值的存在性以及谓词的显式定义（这在许多知识工程任务中至关重要）并不能直接归结为蕴含关系。因此，我们的关注点在于判定给定输入公式、签名和本体中（统一）插值和定义是否存在的计算复杂性。我们证明了：在$\mathsf{Q}^1\mathsf{S5}$和$\mathsf{S5}_{\mathcal{ALC}^u}$中，插值和定义的存在性判定问题属于coN2ExpTime复杂度类，且为2ExpTime-难问题；而统一插值的存在性判定问题不可判定。随后我们证明：在量化模态逻辑$\mathsf{K}$的单变量片段$\mathsf{Q}^1\mathsf{K}$中，插值和定义的存在性判定问题为非线性可判定的，而统一插值的存在性判定问题不可判定。