A Practical Automata-Based Technique for Reasoning in Expressive Description Logics
Diego Calvanese, Domenico Carbotta and Magdalena Ortiz
Different techniques have been proposed for reasoning in expressive, ExpTime-complete Description Logics (DLs), the most prominent of which are tableaux-based calculi and techniques based on automata on infinite trees. While the former provide the basis for most of the currently implemented state-of-the-art DL reasoning systems, the latter are the only ones that provide a robust basis for showing worst-case optimal complexity upper bounds for a wide range of expressive DLs and for various reasoning services. Interestingly, however, up to now automata-based techniques have resisted implementation, due to their best-case exponential behaviour. The theoretical results developed in this work represent a first significant step towards the development of practical automata-based techniques for reasoning in an expressive DL. Our method is worst-case optimal and lends itself to an efficient implementation. In order to show the feasibility of our approach, we have realized a first working prototype of a reasoner that is based upon these techniques and exploits calls to a SAT solver. Our prototype is still far from competitive with state-of-the-art systems for expressive DLs, but shows already encouraging results in the experimental evaluations that we have carried out.