A Hybrid Tableau Algorithm for ALCQ
Jocelyne Faddoul, Nasim Farsinia, Volker Haarslev, Ralf Möller · 2008
Abstract. We propose an approach for extending a tableau-based satisfiability algorithm by an arithmetic component. The result is a hybrid satisfiability algorithm for the Description Logic (DL) ALCQ which extends ALC with qualified number restrictions. The hybrid approach ensures a more informed calculus which, on the one hand, adequately handles the interaction between numerical and logical restrictions of descriptions, and on the other hand, when applied is a very promising framework for average case optimizations. 1