A finite basis theorem for the description logic $\mathcal{A}\mathcal{LC}$

Abstract

The main result of this paper is to prove the existence of a finite basis in the description logic $\mathcal{A}\mathcal{LC}$. 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 $\mathcal{E}\mathcal{L}$ and ${\mathcal{E}\mathcal{L}}_{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).