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

Artale, Alessandro, Jung, Jean Christoph, Mazzullo, Andrea, Ozaki, Ana and Wolter, Frank ORCID: 0000-0002-4470-606X (2023) Living Without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions. ACM Transactions on Computational Logic, 24 (4). pp. 1-51.

PDF
main_arxiv.pdf - Author Accepted Manuscript
Download (860kB) | Preview

Official URL: http://dx.doi.org/10.1145/3597301

Abstract

<jats:p> 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 <jats:inline-formula content-type="math/tex"> <jats:tex-math notation="TeX" version="MathJaX">\(\mathcal {ALCO} \)</jats:tex-math> </jats:inline-formula> , <jats:inline-formula content-type="math/tex"> <jats:tex-math notation="TeX" version="MathJaX">\(\mathcal {ALCH} \)</jats:tex-math> </jats:inline-formula> and <jats:inline-formula content-type="math/tex"> <jats:tex-math notation="TeX" version="MathJaX">\(\mathcal {ALCHOI} \)</jats:tex-math> </jats:inline-formula> and corresponding hybrid modal logics. However, living without Beth and Craig makes these problems 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. </jats:p>

Item Type:	Article
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	06 Jun 2023 07:43
Last Modified:	30 Oct 2023 20:20
DOI:	10.1145/3597301
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3170833