Re: comments on OWL test cases

On May 13, Jeremy Carroll writes:
> 
> 
> (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.

Also my thinking - seems trivially (lite ont is a DL ont and has same semantics).

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

I am very much against our inventing new terms like "decisive". The
term complete seems perfectly correct here - we could add complete and
terminating if you insist, but the "terminating" part is often taken
for granted when completeness is claimed (for implementations at
least).

I have to dash now to catch a flight - more later.

Ian


> >
> > 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 Wednesday, 14 May 2003 16:15:24 UTC