Re: Sketch: reasoning conformance levels (was RE: Issue: Add hasValue to OWL Lite)

I don't think there is any reason to say OWL Full is not for reasoners, 
nor have I seen any evidence to date that OWL Full is incomplete, though 
I've noticed several messages that seem to take it for granted.  In fact, 
I believe OWL Full is sound and complete, though intractable as all hell 
I'm sure. 

Therefore I believe the only thing we can say about OWL Full, wrt 
reasoning and reasoners, is that no one knows how to build a reasoner that 
supports all of OWL Full.

Dr. Christopher A. Welty, Knowledge Structures Group
IBM Watson Research Center, 19 Skyline Dr.
Hawthorne, NY  10532     USA 
Voice: +1 914.784.7055,  IBM T/L: 863.7055
Fax: +1 914.784.6078, Email: welty@us.ibm.com




"Jeremy Carroll" <jjc@hplb.hpl.hp.com>
Sent by: www-webont-wg-request@w3.org
11/07/2002 09:35 AM
 
        To:     "Ian Horrocks" <horrocks@cs.man.ac.uk>, "Jim Hendler" 
<hendler@cs.umd.edu>
        cc:     "Dan Connolly" <connolly@w3.org>, "Deborah McGuinness" 
<dlm@ksl.stanford.edu>, "webont" <www-webont-wg@w3.org>
        Subject:        Sketch: reasoning conformance levels (was RE: 
Issue:  Add hasValue to OWL Lite)

 


>
> I'm not sure I understand the question. In particular I'm not sure
> what is meant by "not expected to be able to say..."


Sorry there is an outstanding action against me to explain this part of 
the
idea ...

Sketch is as follows:


OWL offers the following conformance levels:

OWL DL
OWL Lite
[OWL full - not for reasoners]


Language tools without a reasoning capability MAY claim "OWL Lite
conformance" if they handle all OWL Lite constructs and, if appropriate,
provide support for name separation.
Language tools without a reasoning capability MAY claim "OWL DL 
conformance"
if they handle all OWL constructs and, if appropriate, provide support for
name separation.
Language tools without a reasoning capability MAY claim "OWL full
conformance" if they handle all OWL constructs and, if appropriate, 
provide
support for classes-as-instances (i.e. name separation support can be
switched off).

Reasoning components MAY claim "OWL DL reasoning" (aka "complete OWL DL
conformance") if they provide complete reasoning over OWL DL. i.e. An "OWL
DL reasoner" MUST find proofs for all OWL DL inferences. An OWL DL 
reasoner
MAY find proofs for any OWL full deduction.

Reasoning components MAY claim "OWL Lite reasoning" if they provide OWL 
Lite
conformance (i.e. no OWL Lite constructs makes the reasoner fall over, and
name separation is supported) and the reasoner will find proofs for at 
least
... [tbd]. An OWL Lite reasoner MAY find proofs for any OWL Full 
deduction.

Reasoning components MAY claim "most of OWL DL reasoning" if they provide 
at
least OWL Lite reasoning and ... [tbd] (e.g. pass 90% of the tests).

Documents MAY be described as OWL Lite if they do not use any constructs 
not
in OWL Lite, if they respect name separation, and do not require more than
OWL Lite reasoning for the intended use.

Documents MAY be described as OWL DL if they respect name separation, and
conform to the abstract syntax restrictions.
===

The idea, is separate from the semantic theory, which is addressed by both
the OWL DL and OWL Full semantics. We should set reasoners which wish to
claim OWL support specific goals that match the OWL Lite and OWL DL 
labels.
(I don't think its productive at this stage to talk about OWL full).

The OWL Lite label on a reasoner is an explicit admission that it is
Lite-weight. We should IMO choose the OWL Lite conformance level so that 
as
many reasoners as possible can conform. (i.e. we would try to exclude any
inference from being required that was difficult to implement using any of
the standard implementation approaches - OWL Lite as users can expect all
implementations to implement this).

I guess Ian doesn't like this much, its very grubby ...

I am expecting network inference to be the first to produce a complete OWL
DL reasoner, and part of this conformance stuff is to let that have a
distinctive label approved by this group, while having other lesser labels
for other reasoners that aren't as good.

Jeremy

Received on Thursday, 7 November 2002 11:24:33 UTC