Re: comments on OWL test cases

On May 15, Jeremy Carroll writes:
> 
> Ian if you have time please have another look at
> http://www.w3.org/2002/03owlt/editors-draft/draft/#consistencyChecker
> 
> The changes made since the version last week are:
> - new conformance statement requiring documentation of supported datatypes 
> (stating the obvious)
> - new conformance statement concerning correct result with Unsupported 
> datatypes (Unknown in certain circumstances).
> - s/complete/decisive/
> - deletion of "otherwise it is [in]complete"
> - (indentation typo) a new conformance clause SHOULD NOT return Unknown
>   (again stating the obvious, mainly motivated to ensure that the royalty free 
> nature of this WG covers non-trivial techniques)
> 
> 
> On 'decisive'
> > An OWL consistency checker is complete if, whenever its input document
> > is [in]consistent, it would eventually (given unlimited, but finite,
> > resources of memory and time) return the answer '[In]consistent'.
> 
> Pat points out that this use of the word complete is non-standard; (being less 
> up on the terminology than Pat, I was surprised at this assertion, and found:
> 
> http://www.ai.sri.com/snark/tutorial/node3.html
> [[
> In this configuration SNARK is a logically complete theorem prover; that is, 
> if conclusion does follow from the assertions, SNARK will find a proof. 
> Therefore, we know that in this case the assertions do not imply the 
> conclusion. 
> 
> On the other hand, if SNARK runs on for longer than we expect, there is no 
> way, in general, to determine if the conclusion is not valid or if we simply 
> haven't given it enough time.
> ]]
> 
> We are trying to devise a term for what we have been calling a 
> complete OWL Lite Consistency Checker
> and (unless Dan gets his way)
> complete OWL DL Consistency Checker
> 
> but what we mean is not what is written in the SNARK documentation (which I 
> believe is the normal usage).
> Since SNARK is a potential base on which an OWL consistency checker might get 
> written, and noting that Sandro was confused about our terminology here (I 
> think because it was non-standard), I am fairly convinced that Pat has a 
> point.
> 
> I am happy to support proposed minor edits (such as %s/decisive/foobar/g ) at 
> this point, but if we need a rewrite of this section then we will have to 
> postpone the last call vote.

As far as I can see, the only difference between the SNARK usage and
the one we had/have is our stipulation of finite resources - if we
left SNARK running for long enough it will find a proof, so after
"long enough" we can always determine the validity of the
conclusion. Our case is identical, except that we stipulate finite
resources, in particular finite time. 

For decidable languages such as OWL DL, it is usual to assume that
complete means within finite time, so I still think that
%s/decisive/complete/g is the right way to go. If you/Pat insist, we
could say "complete and terminating". It is (in my view,
unnecessarily) long-winded, but better than inventing terms like
"decisive".


As far as datatypes are concerned, the semantics for datatype theories
in S&AS covers both supported and unsupported datatypes - for
unsupported datatypes, the semantics constrain data values to be
interpreted as the same object if they are syntactically identical,
and otherwise as arbitrary data objects.  It is therefore well defined
what it means to be complete/decisive (ugh) w.r.t. a given datatype
theory, regardless of what datatypes are actually used within the
document. Moreover, extending the datatype theory is monotonic in the
sense that it can only further constrain the models (and so lead to
more entailments).

Under these circumstances I'm not sure that the paragraph

    "If the input document uses datatypes (other than in triples with
    predicate owl:cardinality, owl:minCardinality and
    owl:maxCardinality) that are not supported by the datatype theory
    of the consistency checker, and the consistency of the document
    depends on the internals of the unsupported datatypes then an OWL
    consistency checker MUST return Unknown."

is necessary - the semantics of datatype theories was carefully
designed so that this kind of thing would NOT be necessary.

Ian


> 
> Jeremy
> 
> 
> 
>

Received on Thursday, 15 May 2003 10:43:24 UTC