Re: Sketch: reasoning conformance levels

On November 7, Peter F. Patel-Schneider writes:
> 
> From: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>
> Subject: Sketch: reasoning conformance levels (was RE: Issue: Add hasValue to OWL Lite)
> Date: Thu, 7 Nov 2002 15:35:01 +0100
> 
> [...]
> 
> > 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.
> 
> This has to be modified to handle imports constructs.  I suggest that it
> say something like 
> 
>   Reasoning components MAY claim "OWL/DL entailment" (aka "complete OWL/DL
>   conformance") if they compute all entailments between OWL/DL documents
>   that do not contain imports.  Any reasoning component that claims "OWL/DL
>   entailment" must somehow signal that its reasoning may be incomplete if
>   it cannot find an imported document.  An OWL/DL reasoner MAY find proofs
>   for any OWL/Full entailment.
> 
> I prefer using a / so as to prevent confusion in constructs like ``OWL
> Full entailment''.

I think that this wording could usefully be made more precise. In
particular, "compute all entailments between OWL/DL documents" is
rather woolly - it sounds as though a reasoner that says YES to all
entailment would be compliant, and it could be taken to mean that
computing some kind of deductive closure is required (which would be
infinitely large and so not amenable to complete computation).

I suggest something more like "... if, for any two documents A and B
that do not contain imports, it computes (in finite time) that A
entails B iff the entailment follows from the semantics."


> 
> Also, there is no definition for inference or deduction in OWL, only for
> entailment.  (I just went through and removed the single mention to
> inference or deduction in the semantics document, not to confound Jeremy,
> but because I just realized that I should not mention inference or
> deduction in the semantics document.)
> 
> > 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).
> 
> This is, in my opinion, a *terrible* idea.   Reasoning components may, if
> they wish, describe what sort of reasoning they do, but passing 90% of an
> arbitrary and changeable set of tests is not a useful description, and
> certainly should not be sanctioned as an official way of describing a
> reasoner.

You wont be surprised to hear that I also find this a bad idea,
and totally contrary to the stated motivation for having OWL Light -
which was to define a smaller language that was easier to implement.

What now seems to be suggested is that the language is more or less
the same as OWL DL, and that ease of implementation is instead due to
different requirements w.r.t. implementation. Why bother with OWL Lite
at all in this case? Why not just take OWL DL and adjust the
percentage completeness requirement until the the required ease of
implementation is achieved?

As Peter points out, it would be impossible to measure this in any
objective way, and it would be ridiculous to glorify such a
specification with a name.

Ian


> 
> [...]
> 
> > Jeremy
> 
> peter

Received on Thursday, 7 November 2002 16:09:28 UTC