Abox satisfiability reduced to terminological reasoning in expressive description logics

Description Logics knowledge bases axe traditionally divided into a terminological part (Tbox), and an assertional part (Abox). However, most of recent results on practical algorithms are confined to terminological reasoning only. Due to the applications of Description Logics for databases and the so-called "Semantic Web", there is a growing interest for practical algorithms for Abox reasoning. In this paper we present an algorithm for deciding knowledge base satisfiability based on the idea of separating terminological and assertional reasoning. This modularity allows to build complete Description Logics systems, by reusing available terminological reasoners.