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

NO, it may not. FOL is really  not decideable, even with unlimited 
resources, and so the failure of SNARK to find a proof, even if it is 
allowed to run for ever with infinite memory, is not an indication 
that no proof exists.

>, so after
>"long enough" we can always determine the validity of the
>conclusion.

That is not true. YOu are just misusing the notion of completeness.

>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.

I insist that we do not use a word with an established meaning in a 
nonstandard way. "Complete" used in the context of consistency or 
entailment checking has a very precisely defined meaning. Either we 
stick to that, or we use a different term.

>  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".

I think it is better to use an invented term when we are giving it a 
new meaning, as it avoids accidental mis-use of existing terminology. 
If you wanted to convey the intended meaning using existing 
terminology then it I have suggested a way to do that. "complete and 
terminating" is ambiguous and potentially misleading.

Pat

>
>
>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
>>
>>
>>
>>


-- 
---------------------------------------------------------------------
IHMC					(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola              			(850)202 4440   fax
FL 32501           				(850)291 0667    cell
phayes@ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam@ai.uwf.edu   for spam

Received on Thursday, 15 May 2003 12:07:55 UTC