Tableaux Algorithms for Expressive Possibilistic Description Logics

Possibilistic Description Logics (DLs) extend description logics with possibilistic semantics to reason with inconsistent and uncertain knowledge. In possibilistic DLs, a crucial reasoning task is to compute the inconsistency degree of a possibilistic DL knowledge base. In this work, we first point out a shortcoming of a previous tableaux algorithm for possibilistic DL ALC and propose a new tableaux algorithm. We then propose a tableaux algorithm for computing the inconsistency degree of a knowledge base in possibilistic DL ALCI(R⁺), which extends possibilistic DL ALC with inverse roles and transitive roles. A blocking condition is proposed to ensure the termination of the algorithm. Although the tableaux algorithm for possibilistic DL ALCI(R⁺) is easy to understand and to implement, it may need exponential space in the worst case. Therefore, we give another tableaux algorithm to improve it and show that the complexity of this algorithm is PSpace-complete. This shows that the flexibility in representing uncertain information is handled without extra computational costs.