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

TL;DR

This paper investigates the decidability and complexity of interpolant and explicit definition existence in description and hybrid modal logics with nominals and role inclusions, even without the Craig and Beth properties.

Contribution

It proves that existence of interpolants and explicit definitions is decidable in certain description logics without Beth and Craig, and analyzes their computational complexity and algorithms.

Findings

Existence problems are 2ExpTime-complete with ontologies or universal modality.

Existence problems are coNExpTime-complete without ontologies.

An algorithm for computing interpolants and explicit definitions is provided.

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.