A Hybrid Tableau Algorithm for ALCQ

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.

• Type: Conference
• Year: 2008
• Where: DLOG
• Authors: Jocelyne Faddoul, Nasim Farsinia, Volker Haarslev, Ralf Möller
• Keywords: Automated Reasoning, DLOG 2008, Hybrid Satisfiability Algorithm, Satisfiability Algorithm, Tableau-based Satisfiability Algorithm