A finite basis theorem for the description logic ${\cal ALC}$

TL;DR

This paper proves that in the description logic ALC, the set of GCIs in a finite model always has a finite basis, and provides an algorithm to compute it, extending previous results to more expressive logics.

Contribution

It establishes a finite basis theorem for ALC GCIs and offers a correct algorithm for computing this basis, extending prior work on less expressive logics.

Findings

Finite basis exists for GCIs in finite models of ALC.

An algorithm for computing the finite basis is provided and proven correct.

The theorem extends to finitely generated complete covarieties.

Abstract

The main result of this paper is to prove the existence of a finite basis in the description logic ${\cal ALC}$. We show that the set of General Concept Inclusions (GCIs) holding in a finite model has always a finite basis, i.e. these GCIs can be derived from finitely many of the GCIs. This result extends a previous result from Baader and Distel, which showed the existence of a finite basis for GCIs holding in a finite model but for the inexpressive description logics ${\cal EL}$ and ${\cal EL}_{gfp}$. We also provide an algorithm for computing this finite basis, and prove its correctness. As a byproduct, we extend our finite basis theorem to any finitely generated complete covariety (i.e. any class of models closed under morphism domain, coproduct and quotient, and generated from a finite set of finite models).