A Tableau Decision Procedure for ALC With Monotonic Modal Operators and Constant Domains
Makaleler > Tam Makale · 2009
Yazarlar: Inanç Seylan, Rıza Cenk ERDUR
Electronic Notes in Theoretical Computer Science, SCI Expanded İndekslerine Giren Dergi, Uluslararası, Scopus, 2009, cilt 231, ss 113-130
DOI: 10.1016/j.entcs.2009.02.032
Özet
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.