Re: comments on OWL test cases

(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