We present a novel hybrid architecture for reasoning about description logics supporting role hierarchies and qualified cardinality restrictions (QCRs). Our reasoning architecture is based on saturation rules and integrates integer linear programming. Deciding the numerical satisfiability of a set of QCRs is reduced to solving a corresponding system of linear inequalities. If such a system is infeasible then the QCRs are unsatisfiable. Otherwise the numerical restrictions of the QCRs are satisfied but unknown entailments between qualifications can still lead to unsatisfiability. Our integer linear programming (ILP) approach is highly scalable due to integrating learned knowledge about concept subsumption and disjointness into a column generation model and a decomposition algorithm to solve it. Our experiments indicate that this hybrid architecture offers a better scalability for reasoning about QCRs than approaches combining both tableaux and ILP or applying traditional (hyper)tableau methods.
展开▼
