RE: SEM: All OWL reasoners will be incomplete?

On September 6, Jeremy Carroll writes:
> 
> 
> > Given a sufficiently expressive language (i.e., one like OWL), this
> > doesn't represent any restriction w.r.t. what you ask for below, i.e.,
> > being able to determine if ontology O1 models ontology O2. This is
> > trivially reducible to ontology consistency.
> 
> IIUC only if you can negate an Ontology.
> 
> not(prop rdf:type owl:TransitiveProperty )
> 
> is not in OWL.

No, but it is easy to capture the meaning in OWL. We just assert that
there is some (fresh) individual related via a foo-foo chain to
another (fresh) individual such that the first individual is not
directly foo-related to the second.

> >                 Similarly
> > for a DL, the frame axioms might state that there is a subset of the
> > set of all property names (the transitive properties) whose
> > interpretations must be transitively closed. 
> 
> In terms of Pat's document then
> 
> If E is:
> owl:TransitiveProperty
> then x is in ICEXT(I(E)) iff:
> <y, z> and <z, u> in IEXT(x) implies <y, u> in IEXT(x)
> 
> should be weakened to
> 
> If E is:
> owl:TransitiveProperty
> then [[ x is in ICEXT(I(E)) implies
> { <y, z> and <z, u> in IEXT(x) implies <y, u> in IEXT(x) }
> ]]
> 
> 
> 
> I still haven't understood which way you prefer to go on this.
> Sorry. (I found your message quite difficult :( ).

I didn't express a preference. I just said that we need to
decide.

> e.g.
> >Having said that, the expressive power of OWL means that entailment
> >w.r.t. ontologies containing property inclusion and transitivity
> >axioms is still trivially reducible to ontology consistency.
> 
> Could you please give an example:
> 
> e.g.
> 
> { empty }
> does not entail
> { foo rdf:type owl:TransitiveProperty }
> 
> how do I convert that into a consistency question?

Given the iff semantics for TransitiveProperty, foo rdf:type
owl:TransitiveProperty is entailed by an ontology Ont if adding the
following axiom:

type(x, intersectionOf(someValuesFrom(foo, someValuesFrom(foo, oneOf(y))),
                       allValuesFrom(foo, not(oneOf(y)))))

to Ont would make it unsatisfiable.

As this is clearly not the case w.r.t. an empty ontology, then the
entailment does not follow.

As you can see, this is more or less like using OWL to check if:

exists x,w,y (foo(x,w) ^ foo(w,z) ^ not(foo(x,z)))

is unsatisfiable.

Ian


> 
> Jeremy

Received on Sunday, 8 September 2002 20:28:48 UTC