Re: LANG: inverse/onOf interaction

Ian Horrocks wrote:
> 
> 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).


Ian, I don't get it. Where is oneOf used in this example? It seems that
the combination of hasValue, cardinality, and inverse is what leads to
this case, not inverse and oneOf. Did you leave something out, or am I
missing something?

Jeff

> 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 09:27:48 UTC