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

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).