Artale, Alessandro, Jung, Jean Christoph, Mazzullo, Andrea, Ozaki, Ana and Wolter, Frank 
ORCID: 0000-0002-4470-606X
(2021)
Living Without Beth and Craig: Definitions and Interpolants in Description Logics with Nominals and Role Inclusions.
THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 35.
pp. 6193-6201.
ISSN 2159-5399, 2374-3468
|
PDF
2007.02736v5.pdf - Submitted version Download (765kB) | Preview |
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 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.
| Item Type: | Article |
|---|---|
| Additional Information: | We have revised a few sections from the previous version. The relationship between interpolants and explicit definitions is analysed in more detail now |
| Uncontrolled Keywords: | cs.LO, cs.LO, 03B70 |
| Divisions: | Faculty of Science and Engineering Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 07 Nov 2024 14:25 |
| Last Modified: | 07 Nov 2024 14:25 |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3187110 |
Share
Share
