TY - JOUR AU - Artale, Alessandro AU - Jung, Jean Christoph AU - Mazzullo, Andrea AU - Ozaki, Ana AU - Wolter, Frank PY - 2021/05/18 Y2 - 2024/03/29 TI - Living Without Beth and Craig: Definitions and Interpolants in Description Logics with Nominals and Role Inclusions JF - Proceedings of the AAAI Conference on Artificial Intelligence JA - AAAI VL - 35 IS - 7 SE - AAAI Technical Track on Knowledge Representation and Reasoning DO - 10.1609/aaai.v35i7.16770 UR - https://ojs.aaai.org/index.php/AAAI/article/view/16770 SP - 6193-6201 AB - 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 transform potentially hard existence problems into deduction problems in the underlying logic. Description Logics with nominals and/or role inclusions do not enjoy the CIP nor PBDP, but interpolants and explicit definitions have many potential applications in ontology engineering and ontology-based data management. In this article we show the following: even without Craig and Beth, the existence of interpolants and explicit definitions is decidable in description logics with nominals and/or role inclusions such as ALCO, ALCH and ALCHIO. However, living without Craig and Beth makes this problem harder than deduction: we prove that the existence problems become 2EXPTIME-complete, thus one exponential harder than validity. The existence of explicit definitions is 2EXPTIME-hard even if one asks for a definition of a nominal using any symbol distinct from that nominal, but it becomes EXPTIME-complete if one asks for a definition of a concept name using any symbol distinct from that concept name. ER -