Re: comments on OWL test cases

On May 13, Jeremy Carroll writes:
> 

[snip]

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

To add to my earlier comment. I am (still) not keen on inventing terms
like "decisive", and I believe that it is adding an unnecessary
complication. Why not simply say:

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

Of course we also need to add in some text about supported datatypes.

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

All seems pointless to me. How are we to know if an implementation is
telling the truth about the reason for its failure to compute the
answer, and why should we care?


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

The way things are set up now effectively allows a different (set of
if we consider Lite/DL/Full) OWL species to be defined for all
possible combinations of supportable datatypes. Implementors can pick
any one of these species. Completeness is (well) defined w.r.t. the
chosen species.

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

This doesn't seem and unreasonable requirement :-), in fact it is hard
to imagine any implementation NOT meeting it (users have to guess
which datatypes are supported?).

[snip]

Regards, Ian

Received on Wednesday, 14 May 2003 19:31:06 UTC