01436nas a2200169 4500008004100000245006200041210006000103260003300163300001200196490000900208520092100217100001901138700002001157700001901177700002001196856005001216 2009 eng d00aA Preferential Tableaux Calculus for Circumscriptive ALCO0 aPreferential Tableaux Calculus for Circumscriptive ALCO aChantilly, VA, USAbSpringer a40–540 v58373 a

Nonmonotonic extensions of description logics (DLs) allow for default and local closed-world reasoning and are an acknowledged desired feature for applications, e.g. in the Semantic Web. A recent approach to such an extension is based on McCarthy’s circumscription, which rests on the principle of minimising the extension of selected predicates to close off dedicated parts of a domain model. While decidability and complexity results have been established in the literature, no practical algorithmisation for circumscriptive DLs has been proposed so far. In this paper, we present a tableaux calculus that can be used as a decision procedure for concept satisfiability with respect to conceptcircumscribed ALCO knowledge bases. The calculus builds on existing tableaux for classical DLs, extended by the notion of a preference clash to detect the non-minimality of constructed models.

1 aGrimm, Stephan1 aHitzler, Pascal1 aPolleres, Axel1 aSwift, Terrance uhttp://dx.doi.org/10.1007/978-3-642-05082-4_4