Re: non-entailment test for imports

From: Jim Hendler <hendler@cs.umd.edu>
Subject: non-entailment test for imports (was Re: Proposed response to Golbeck regarding imports issue)
Date: Tue, 17 Jun 2003 09:50:29 -0400

> At 2:29 PM +0100 6/17/03, Ian Horrocks wrote:
> >Jim,
> >
> >Quoting from Test:
> >
> >     An OWL Lite or OWL DL document D is consistent with respect to a
> >     datatype theory T if and only if there is some abstract OWL
> >     interpretation I with respect to T such that I satisfies an
> >     abstract ontology O equivalent to D, in which O has a separated
> >     vocabulary; (see [OWL Semantics and Abstract Syntax]).
> >
> >     An OWL Full document D is consistent with respect to a datatype
> >     theory T, if and only if there is some OWL Full interpretation I
> >     with respect to T such that I satisfies all the RDF graphs in some
> >     imports closed collection containing an RDF graph equivalent to D.
> >
> >     ...
> >
> >     An OWL consistency checker MUST be sound: it MUST return
> >     Consistent only when the input document is consistent and
> >     Inconsistent only when the input document is not consistent, with
> >     respect to the datatype theory of the checker.
> >
> 
> 
> I will answer this one in this WG (instead of moving to rdf-logic) 
> because I think it is VERY important to our design -- as I understand 
> our tests, the entailment tests MUST agree that something is 
> entailed.  However, it is my understanding that the non-entailment 
> tests do not require stating that a contradiction occurs, they may 
> return "Unknown" -- so if I want to pass the imports002 test but do 
> what Dan does, I could simply note that it includes a pointer to a 
> non-imported namespace and that the entailment occurs there,and 
> therefore I can imagine a tool producing a proof that essentially 
> says:
> 
> This document alone may not entail XXX, however it points to another 
> document that, if imported, would entail XXX.
> 
> 
> This first statement above (may not entail XXX) would mean it passed our test.
> 
> This would be within the letter and the law of our design (and maybe 
> even the spirit of the design for some of us).

Well, given that there is no definition of an entailment checker in the
test document, I guess that nothing can really be said here.

However, if there was a definition of a compete OWL Lite entailment
checker, it would have to be worded something like this:

	A complete OWL Lite entailment checker takes two OWL Lite documents
	as input.  If the first document entails the second then the
	checker returns TRUE, otherwise the checker returns FALSE.

A complete OWL Lite entailment checker would then be obligated to return
FALSE on owl:imports tests 0002.  Any other return would be in error.  

Of course, if the checker was helpful, it might return (in some out-of-band
fashion) the helpful response

	The entailment would be true if the premise included an imports of
	the document ....  The entailment would also be true if the premise
	included the conclusion.  The entailment would also be true
	.... ... 

> If I am wrong on this, then I am very worried about our design of the 
> imports002 test, and will consider that this may be new evidence that 
> would convince me to ask Guus to reopen the imports issue.  If I'm 
> right, then I don't care if you think the above is a bad way to lead 
> my life, I just want to make sure that we have not ruled out 
> something that the chair believes the WG agreed not to rule out.

>   -JH

peter

Received on Tuesday, 17 June 2003 10:54:06 UTC