- From: Jeremy Carroll <jjc@hpl.hp.com>
- Date: Tue, 13 May 2003 20:57:38 +0300
- To: www-webont-wg@w3.org
(This message predates http://lists.w3.org/Archives/Public/www-webont-wg/2003May/0168.html and gives a different tale on datatypes - I will look at the decision in the issues list next ) Hmm it seems I will have to do more work than I had been planning at this stage ... > 4.2.1 (suggestion) Might be better to allow a syntax checker to > ignore some lower levels, eg I'd be very happy with an engine that > would say 'DL' for Lite docs as well as DL-not-Lite ones. I am not accepting this suggestion. Rationale: that may be a useful tool, there are many useful tools we could have defined. The one we did define is not, prehaps, very useful. I do not believe the motive for these definitions is their fundamental utility but more they are simple to state and give developers a common target. Given the (im)maturity of the area we would then expect developers to have their own spin on other functionality. As an example, the syntax checker I wrote gives error messages consisting of (hopefully) small subgraphs that are not in OWL Lite, or not in OWL DL, if so desired. I hope this is useful, but I wouldn't expect it to be standardised. I have already had demand for an OWL parser , which I take to be a device that returns an abstract syntax tree from RDF/XML output. That I think is what some users will want - however I am not convinced that we should make the abstract syntax obligatory in such a way. I believe that the current syntax checker specification is sufficient to give some idea of what we expect, without being overly spelled out (i.e. the spelling out that we have done is clearly insufficient for most purposes). > 4.2.2 > Er... I'm embarrassed that I don't know the answer to this, but is it > really the case that any Lite ontology is consistent in Lite iff it > is consistent in Full? Is there a proof of that somewhere? Sandro suggested deleting the line "Every OWL Lite consistency checker can be trivially transformed into an OWL Full consistency checker. " I take the rest of the note to follow from the semantic layering results and the correspondence theorem. (Actually, these results are currently false - see thread concerning intersectionOf bug). > [Added later: I see that you credit Ian with help on this section. I > think the three of us could agree on a suitable wording reasonably > quickly.] I think the usual convention is that Ian gets the credit and I get the blame! Any faults should be attributed to me. > So I would suggest the following: > distinguish a consistency checker (responses are Con/unknown) from an > inconsistency checker (Incon/unknown), and define 'complete' for both > of them thus: > A[n in]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'. > Then say a checker is decisive (new word, avoids the 'decision > procedure' terminology) if it is both a complete consistency checker > and a complete inconsistency checker. Then remark that there are no > decisive checkers for OWL-Full but there are for OWL-Lite and OWL-DL. > > Simpler (editorial) option: replace 'complete' with 'decisive' (or > some other word which is not a standard logical term) in current > definition and rest of text. I am inclined to do the second of these, I will give more detail after I have touched the text. IMO we already have too many consistency checkers defined (5) Your first suggestion would increase this number. > Another idea: allow three responses (four for a double-sided checker) > where 'unknown' means 'dunno, run out of energy' and 'indeterminate' > means 'can't figure because of network error or some such'. Then you > could allow a complete implementation to return 'indeterminate' but > not 'unknown'. Roughly, this distinguishes inability to answer based > on internal versus external issues. Completeness relative to > externals is obviously impossible to guarantee, is the point. Sandro, too, wanted some change on this point. (He wanted "ResourceLimitExceeded" as a legal response). How about: [[ Consistency checkers MAY return additional information. For example, the response 'Unknown' may have special cases such as 'Unknown (time-limit-exceeded)', ''Unknown (memory limit exceeded)', 'Unknown (infinite model checking not implemented)'. ]] > Im a bit worried about stating completeness in the presence of > datatypes. So was I. > Does this mean that consistency wrt one set of datatypes > is different from consistency wrt a different set? ******* This text here was written early this morning and gives one view of what a datatype theory is. The msg http://lists.w3.org/Archives/Public/www-webont-wg/2003May/0168.html was written later after I had reread the S&AS text on datatype theory. I would appreciate someone else opinion as to which of these readings is correct. ************** I think it might be. For example, xsd:NMToken is a subdatatype of xsd:string. However, we do not require implementations to know that. Thus <FunctionalProperty rdf:ID="dp"> <owl:Thing> <dp rdf:datatype="&xsd;NMToken">1</dp> <dp rdf:datatype="&xsd;NMToken">01</dp> </owl:Thing> is inconsistent if you know that the l2v mapping of the datatype is the identity. But if you don't then maybe xsd:NMToken is derived from integer, and the file is consistent. As I understand it, S&AS, with a datatype theory that does not include xsd:NMToken, makes the above example consistent. With a datatype theory that does include xsd:NMToken then the above example is inconsistent. I have not provided any tests for the former statement, or analogous; and don't currently intend to. > I think > this needs to be spelled out a little more carefully (define it wrt a > datatype API, maybe? ) I could add a statment like [[ An OWL consistency checker MUST provide a means to determine the datatypes supported by its datatype theory; for example, by listing them in its supporting documentation. ]] > The final NOTE in this section refers only to DL and Lite: why? This > is characteristic of all forms of completeness. We only agreed to define complete OWL Lite and OWL DL consistency checkers (Manchester f2f). There is no complete OWL Full consistency checker (your term 'decisive') since OWL Full is not decidable. >Why are there not parallel definitions of an entailment checker, with >conforming definitions of completeness, correctness etc. ? It would >seem to be easy enough to state these in parallel to those in section >4.2. These notions would be a lot more useful in practice I notice you missed the Manchester f2f - we did have a fairly heated debate. (The Friday morning session ended somewhat abruptly with most of the current ideas on the table but not with consensus - I had a long lunch catching up with an old friend, and when I returned the group had made much more progress without me). So the brief response is "WG decision" There was reluctance to have any software conformance statements. There were others who strongly desired software conformance statements. There was agreement that we were obliged to provide document conformance statements. The agreed software conformance statements hang off the document conformance statements. As one of the people in favour of s/w conformance statements I came away happy for the following reasons: - anyone building a consistency checker will have the bits and pieces to construct an entailment tool - it is (slightly) less clear what an entailment tool should do - assuming an entailment tool is genuinely useful someone who has built a consistency checker to get the OWL conformance sticker, will also supply an entailment tool. - given that we have entailment tests in the test suite it is likely that most tool developers will, internally at least, make the effort to provide such functionality, if only to take full advantage of the test suite. - as test editor I could ensure that many tests were consistency and inconsistency tests, and have fewer entailment tests (This is a policy I have actively pursued since the Manchester f2f). Jeremy
Received on Tuesday, 13 May 2003 14:57:29 UTC