- From: Ian Horrocks <horrocks@cs.man.ac.uk>
- Date: Thu, 13 Jun 2002 13:33:25 +0100 (BST)
- To: www-webont-wg@w3c.org
I promised to explain in a bit more detail why inverse properties and oneOf interact adversely (at least as far as reasoning support is concerned). The combination of these features is very powerful, and it is easy to see how they can be used to build ontologies for which reasoning will be very difficult. One example is the use of a so called "spy-point" to limit the maximum size of the domain of discourse. This is done, e.g., as follows: 1. Add an axiom asserting that every element in the domain of discourse is related to the individual "Spy" via some property, i.e., add the axiom Thing subClassOf (hasValue P Spy). 2. Add an axiom asserting that Spy is related to at most n distinct individuals via the inverse of the P property, i.e., Spy type (maxCardinality (inverse P) n). It may be counter-intuitive, but the ability to fix the size of the domain of discourse to some arbitrary size makes reasoning much harder. From a practical point of view, this can be seen in many "strange" additional inferences: e.g., for ANY property R, the class defined by a restriction (minCardinality R n+1) becomes incoherent (because there can only be n distinct objects in the domain of discourse). From a theoretical point of view, the worst case complexity of basic inference tasks (e.g., class consistency) jumps from Exptime (for DAML+OIL without inverse or without oneOf), to NExpTime for full DAML+OIL. If fact, inference is already NExpTime hard for the basic ALC description logic (booleans plus hasClass and toClass) with the addition of inverse and oneOf. In fact, the problem boils down to the loss of the tree model property. The language without oneOf has the (transitive) tree model property, that is, any class that has a model has a (transitive) tree model. This means that decision procedures can restrict their attention to this kind of model without sacrificing completeness/corectness. With oneOf but no inverse, things are a bit more complex, but a similar restriced model property can be demonstrated. You can find some more information, including pointers to various other relevant papers, in [1] (sorry for the self citation). I hope this helps - no doubt you will let me know if you have any queries. Ian [1] http://www.cs.man.ac.uk/~horrocks/Publications/download/2001/ijcai01.pdf
Received on Thursday, 13 June 2002 08:32:46 UTC