Affiliations: Department of Computer Science and Software Engineering, Concordia University, Montreal, QC, Canada
Note: [] Corresponding author: Volker Haarslev, Department of Computer Science and Software Engineering, Concordia University, 1455 de Maisonneuve Blvd. W., Montreal, QC H3G 1M8, Canada. E-mail: haarslev@cse.concordia.ca.
Abstract: This article presents a hybrid Abox tableau calculus for ๐ฎโ๐ฌ which extends the basic description logic ๐โ๐ with role hierarchies, transitive roles, and qualified number restrictions. The prominent feature of our hybrid calculus is that it reduces reasoning about qualified number restrictions to integer linear programming. The calculus decides ๐ฎโ๐ฌ Abox consistency w.r.t. a Tbox containing general axioms. The presented approach ensures a more informed calculus which adequately handles the interaction between numerical and logical restrictions in ๐ฎโ๐ฌ concept and individual descriptions. A prototype reasoner for deciding ๐โ๐โ๐ฌ concept satisfiability has been implemented. An empirical evaluation of our hybrid reasoner and its integrated optimization techniques for a set of synthesized benchmarks featuring qualified number restrictions clearly demonstrates the effectiveness of our hybrid calculus.
Keywords: Description logics, qualified number restrictions, integer linear programming
