Practical reasoning for very expressive description logics (Q4487262)

Description Logics provide a formalization of knowledge representation languages. The formalization is based on the notion of concept (unary predicate) and role (binary predicate). Complex concepts and roles are constructed from atomic ones using some constructors. The language of a description logic, \({\mathcal A}{\mathcal L}{\mathcal C}\), is extended with transitive and inverse roles, role hierarchies, and functional restrictions. There is a relationship of this logic to the propositional (multi)modal logic \({\mathbf S4_{(m)}}\). An algorithm deciding the satisfiability of the extended language is presented. The fact that the algorithm deals only with transitive roles, instead of transitive closure, leads to a lower degree of indeterminism, and experiments indicate that the algorithm is well-suited for implementation. It is shown that the \({\mathcal A}{\mathcal L}{\mathcal C}\) extended with transitive and inverse roles is still in PSPACE. The algorithm uses an enhanced blocking technique. The technique seems to be useful from the viewpoint of efficient implementations of more expressive description logics. The limits of decidability for the considered family of description logics is investigated. It is shown that relaxing the constraints placed on the kinds of roles used in number restrictions leads to undecidability of all inference problems. Some optimization techniques are studied. The techniques are crucial in obtaining implementations of the decision procedures. Computational experiments with the implemented system are described in the concluding section of the paper.