Re: SEM: All OWL reasoners will be incomplete?

On September 4, Jeremy Carroll writes:
> 
> 
> I have just been reading one of the threads that went on while I was on
> holiday.
> 
> i.e.
> OWL semantics
> http://lists.w3.org/Archives/Public/www-webont-wg/2002Aug/thread.html#44
> and also the subthread
> OWL semantics ( with focus on an axiomatization)
> 
> If I have understood Ian correctly
> > Point 1b:
> >
> > It should NOT be possible to use OWL/RDF statements to constrain the
> > meaning of OWL/RDF syntax. E.g., if myTransitive is a sub-class of
> > transitiveProperty, then instances of myTransitive should NOT be
> > treated by OWL as transitive properties. If we go down this road, then
> > we need a (HOL) reasoner even to parse the syntax of an OWL ontology,
> > to determine what is being said, and to check that it is valid OWL.
> ...
> > It may even be IMPOSSIBLE to be sure that we
> > have derived the complete syntactic meaning of an OWL ontology
> > (because the language is undecidable).
> 
> The alternative being that sound and complete reasoners are too difficult to
> build.
> 
> However, the view that complete reasoning is possible in DL is based on a
> restricted idea of what reasoning is (largely class subsumption reasoning,
> and consistency checking)

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.

> So Ian brought up the case in
> 
> http://lists.w3.org/Archives/Public/www-webont-wg/2002Aug/0033.html
> 
> of
> 
> >This is wrong. The MT simply imposes a restriction that, in all
> >models, the interpretation of a TransitiveProperty must be closed
> >under transitivity. This does not mean that any property that is
> >closed under transitivity in all models is necessarily a
> >TransitiveProperty (such a situation could result from other causes,
> >e.g., the properties interpretation being empty in all models, or the
> >size of the domain being less than 3 in all models).
> 
> I find the entailments view of reasoning fairly compelling:
> - an OWL document entails another if every interpretation of the first is
> also an interpretation of the second.
> 
> A complete reasoner should be able to prove any valid entailment.
> 
> Thus, either it is the case that "any property that is closed under
> transitivity in all models is necessarily a TransitiveProperty", or it is
> the case that the concept owl:TransitiveProperty is in the domain of
> discourse in an RDF style.

The normal way these things are handled in description and modal
logics is to have a set of "frame axioms" that constrain the set of
admissible interpretations. These frame axioms are not treated as part
of the KB/theory. E.g., in multi-modal K4, the frame axioms state that
the only admissible interpretations in those in which the
interpretations of all modalities are transitively closed. 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. The KB/theory therefore
doesn't contain any axioms relating to properties, and so the question
of entailments does not arise w.r.t. properties.

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. Thus if
we have a sound and complete reasoner for ontology consistency, we have
a sound and complete reasoner for ontology entailment.

The point w.r.t. transitive properties is simply that, if we don't
take the frame axiom view, and decide instead that we can infer the
transitivity of a role, then we need to be a little more careful about
how we state the restriction w.r.t. the use of transitive properties
in cardinality restrictions. This is not a serious problem - just
something we have to take care of.

It is a completely different thing if we can infer the existence of an
axiom asserting that a property is transitive (as would be the case if
OWL syntax were in the domain of discourse). In this case, we need to
perform inference (in a language which is almost certainly
undecidable) on the ontology in order to determine if it conforms with
our definition of what is a syntactically valid ontology. I was
suggesting (in point 1b) that we don't want to go there!

Regards, Ian

> So, I am increasingly coming round to thinking that incompleteness is
> inevitable ...
> 
> Jeremy
> 
> 
> 
> 
>

Received on Thursday, 5 September 2002 10:43:45 UTC