We introduce a tableau calculus for a nonmonotonic extension of low complexity Description Logic ℰℒ⊥ that can be used to reason about typicality and defeasible properties. The calculus deals with Left Local knowledge bases in the logic ℰℒ⊥Tmin recently introduced in [8]. The calculus performs a two-phase computation to check whether a query is minimally entailed from the initial knowledge base. It is sound, complete and terminating. Furthermore, it is a decision procedure for Left Local ℰℒ⊥Tmin knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in Π2p. © 2011 Springer-Verlag.
CITATION STYLE
Giordano, L., Gliozzi, V., Olivetti, N., & Pozzato, G. L. (2011). A tableau calculus for a nonmonotonic extension of ℰℒ ⊥. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6793 LNAI, pp. 180–195). https://doi.org/10.1007/978-3-642-22119-4_15
Mendeley helps you to discover research relevant for your work.