SEM: All OWL reasoners will be incomplete?

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)

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.

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

Jeremy

Received on Wednesday, 4 September 2002 13:35:13 UTC