Efficient Reasoning with Range and Domain Constraints

We show how a tableaux algorithm for SHIQ can be extended to support role boxes that include range and domain axioms, prove that the extended algorithm is still a decision procedure for the satisfiability and subsumption of SHIQ concepts w.r.t. such a role box, and show how support for range and domian axioms can be exploited in order to add a new form of absorption optimisation called role absorption. We illustrate the effectiveness of the optimised algorithm by analysing the perfomance of our FaCT++ implementation when classifying terminologies derived from realistic ontologies.

• Type: Conference
• Year: 2004
• Where: DLOG
• Authors: Dmitry Tsarkov, Ian Horrocks
• Keywords: Automated Reasoning, DLOG 2004, Extended Algorithm, Optimisation Called Role, Tableaux Algorithm