The Craig interpolation property (CIP) states that an interpolant for an implication exists iff it is valid. The projective Beth definability property (PBDP) states that an explicit definition exists iff a formula stating implicit definability is valid. Thus, the CIP and PBDP reduce potentially hard existence problems to entailment in the underlying logic. Description (and modal) logics with nominals and/or role inclusions do not enjoy the CIP nor the PBDP, but interpolants and explicit definitions have many applications, in particular in concept learning, ontology engineering, and ontology-based data management. In this article we show that, even without Beth and Craig, the existence of interpolants and explicit definitions is decidable in description logics with nominals and/or role inclusions such as ALCO, ALCH and ALCHOI and corresponding hybrid modal logics. However, living without Beth and Craig makes this problem harder than entailment: the existence problems become 2ExpTime-complete in the presence of an ontology or the universal modality, and coNExpTime-complete otherwise. We also analyze explicit definition existence if all symbols (except the one that is defined) are admitted in the definition. In this case the complexity depends on whether one considers individual or concept names. Finally, we consider the problem of computing interpolants and explicit definitions if they exist and turn the complexity upper bound proof into an algorithm computing them, at least for description logics with role inclusions.

翻译：克雷格插值性质（CIP）断言：蕴涵式的插值存在当且仅当其有效。投影贝斯可定义性性质（PBDP）断言：显式定义存在当且仅当表述隐式可定义性的公式有效。因此，CIP和PBDP将潜在困难的存在性问题归约为底层逻辑中的蕴含判定。带名词和/或角色包含的描述逻辑（及模态逻辑）不满足CIP或PBDP，但插值和显式定义在概念学习、本体工程和基于本体的数据管理等领域具有广泛应用。本文证明，即便没有Beth和Craig性质，在带名词和/或角色包含的描述逻辑（如ALCO、ALCH和ALCHOI）及相应混合模态逻辑中，插值和显式定义的存在性仍是可判定的。然而，无Beth和Craig使该问题比蕴含判定更困难：当存在本体或全域模态时，存在性问题成为2ExpTime完全问题，否则为coNExpTime完全问题。本文还分析了允许所有符号（除被定义符号外）参与定义时的显式定义存在性，此时复杂度取决于所考虑的是个体名还是概念名。最后，我们探讨了插值和显式定义存在时的计算问题，并将复杂度上界证明转化为计算算法——至少对于带角色包含的描述逻辑而言。