- From: Ian Horrocks <horrocks@cs.man.ac.uk>
- Date: Thu, 15 May 2003 15:54:08 +0100
- To: Jeremy Carroll <jjc@hpl.hp.com>
- Cc: www-webont-wg@w3.org

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