A constraint-based decision procedure for the description logic ALCN

Abstract

Description logics are modal-like logics used to express knowledge about structured domains, and reason about them. One of the major reasoning problems in description logics is that of determining whether a given terminological knowledge base is consistent. One approach to this problem is to translate a modal satisfiability problem into stratified layers of constraint problems that can be solved by a constraint solver. We show how this approach, which was originally developed for the modal logic K, can be extended to deal effectively with cardinality restrictions on roles in the description logic ALCN. We also propose a further extension to this approach in order to deal with qualified number restrictions and arithmetic on role cardinalities. © 2006 SAICSIT.