Computation of Interpolants for Description Logic Concepts in Hard Cases

TL;DR

This paper introduces elementary algorithms for computing ALC-interpolants in description logics, especially in challenging cases where the logic does not have the Craig Interpolation Property, highlighting potential size issues.

Contribution

It provides the first algorithms for computing ALC-interpolants under more expressive ontologies and concepts, addressing gaps in existing methods.

Findings

Algorithms for ALC-interpolants under ALCH and ALCQ ontologies

Interpolant size can be non-elementary in some cases

Decision procedures enable interpolant existence checks

Abstract

While the computation of Craig interpolants for description logics (DLs) with the Craig Interpolation Property (CIP) is well understood, very little is known about the computation and size of interpolants for DLs without CIP or if one aims at interpolating concepts in a weaker DL than the DL of the input ontology and concepts. In this paper, we provide the first elementary algorithms computing (i) ALC-interpolants between ALC-concepts under ALCH-ontologies and (ii) ALC-interpolants between ALCQ-concepts under ALCQ-ontologies. The algorithms are based on recent decision procedures for interpolant existence. We also observe that, in contrast, uniform (possibly depth restricted) interpolants might be of non-elementary size.