A Tableau Decision Procedure for ALC With Monotonic Modal Operators and Constant Domains

Modal description logics provide a more expressive framework than their propositional counterparts by allowing one to define the individuals and concepts of a particular application domain. In the literature, tableau decision algorithms have been given for various normal modal and temporal description logics. There is however a trend towards the use of coalition logics in the intelligent agents community. Coalition logics are extensions of the basic monotonic modal logic M which is a non-normal modal logic. This paper presents a tableau decision procedure for the formula satisfiability problem of the constant domain variant of MALC, i.e., ALC extended with modal operators from M that can be applied both to formulas and concepts. The presented algorithm can be used as the basis of a tableau decision procedure for coalition description logic.