Living Without Beth and Craig: Definitions and Interpolants in Description Logics with Nominals and Role Inclusions

Authors

  • Alessandro Artale Free University of Bozen-Bolzano
  • Jean Christoph Jung University of Hildesheim
  • Andrea Mazzullo Free University of Bozen-Bolzano
  • Ana Ozaki University of Bergen
  • Frank Wolter University of Liverpool

Keywords:

Description Logics, Computational Complexity of Reasoning

Abstract

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.

Downloads

Published

2021-05-18

How to Cite

Artale, A., Jung, J. C., Mazzullo, A., Ozaki, A., & Wolter, F. (2021). Living Without Beth and Craig: Definitions and Interpolants in Description Logics with Nominals and Role Inclusions. Proceedings of the AAAI Conference on Artificial Intelligence, 35(7), 6193-6201. Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/16770

Issue

Section

AAAI Technical Track on Knowledge Representation and Reasoning