Re: Datatypes - help please

On March 26, Jeremy Carroll writes:
> 
> 
> I am trying to understand what I need to change in the test document to 
> reflect WG decisions vis-a-vis datatypes.
> 
> I believe I should be working from Ian's text in
> http://lists.w3.org/Archives/Public/www-webont-wg/2003Mar/0045.html
> 
> I have some minor additions  (see * * text)
> specifically:
> 
> [[
> OWL Consistency Checkers
> ========================
> 
> An OWL consistency checker takes a document as input, and outputs one
> word: Consistent, Inconsistent, or Unknown.
> 
> An OWL document is Consistent iff there exists some MODEL of the
> document that is consistent with the constraints specified by the
> relevant MODEL THEORY (*see ASS <link>OWL Lite and OWL DL</link>, <link>OWL 
> Full</link>).
> 
> An OWL consistency checker MUST return "Consistent" only when the
> input document is consistent and "Inconsistent" only when the input
> document is not consistent (this property is usually called
> SOUNDNESS).
> 
> An OWL consistency checker is COMPLETE, **with respect to its
> supported datatypes**, if, given sufficient (but
> finite) resources (CPU cycles and memory), it will always return
> either Consistent or Inconsistent **(for an input document
> that does not use any unsupported datatypes)**; 

NO this is NOT correct. The S&AS defines consistency w.r.t. a DATATYPE
THEORY. A datatype theory "supports" certain datatypes, which
basically means that it interprets the lexical forms of data values
according to the SEMANTICS of the datatype (in particular equality and
inequality are correctly handled); for unsupported datatypes, the
lexical forms of data values are interpreted according to their SYNTAX
(two values are equal if the strings are identical, otherwise they may
or may not be equal). I would suggest:

   A consistency checker is COMPLETE w.r.t. datatypes supported by its
   datatype theory, if, given sufficient (but finite) resources (CPU
   cycles and memory), it will always return either Consistent or
   Inconsistent.

There is NO REQUIREMENT for the document to exclude "unsupported"
datatypes - this is the beauty of the new formalisation. For a
consistency checker supporting more datatypes, there will simply be
more valid inferences, and so fewer consistent documents. All can
claim, however, to be complete w.r.t. their own datatype theory (if
the rest of the checker is complete, of course).


> otherwise it is INCOMPLETE. It has
> been shown that for OWL Lite and DL it is possible to construct a
> complete consistency checker (the languages are DECIDABLE), and that
> for OWL full it is not possible to construct a complete consistency
> checker (the language is UNDECIDABLE).
> 
> An OWL consistency checker SHOULD minimally support at least 
> the following XMLS datatypes: integer, string.

I suggest:

	An OWL datatype theory SHOULD minimally support at least the
	following XMLS datatypes: integer, string.


> ]]
> 
> is that enough?
> is there a link for the word "support" in the last paragraph to S&AS?

I suggest the following link (for datatype theories):

http://www-db.research.bell-labs.com/user/pfps/owl/semantics/semantics-all.html#3.1


> 
> I would continue with the exact characterisation of the five consistency 
> checkers agreed at the January f2f (text largely unchanged from current WD).

The last 2 (complete Lite/DL) are rather inconsistent/confusing
w.r.t. the above definition of completeness. It would be better to
simply say:

       A complete OWL Lite consistency checker is an OWL Lite consistency
       checker that is complete.

       A complete OWL DL consistency checker is an OWL DL consistency
       checker that is complete.

Ian

> 
> Jeremy
> 
>

Received on Wednesday, 26 March 2003 18:57:38 UTC