Datatypes in test (attn Ian, Pat, Sandro) RE: comments on OWL test cases

In response to Pat:

http://lists.w3.org/Archives/Public/www-webont-wg/2003May/0166.html
comments on OWL test cases

I seemed to have mislaid an earlier drafted reply to much of this message -
I will be able to find it in about 10 hours time.

I will highlight one issue here that is worth discussing.
Pat:
> [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.]

Let's follow the usual convention in which Ian gets any credit
and I get any blame.

> 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 prefer this to the other suggestion, rationale (against the more extensive
suggestions) later today.
We could add a note that captures some of your comment about asymmetry.

Pat:
> Im a bit worried about stating completeness in the presence of datatypes.
> Your definition is behavioral - it talks about what the software
> delivers -
> and it uses the words 'with respect to datatypes'. Does this mean that
> consistency wrt one set of datatypes is different from consistency wrt a
> different set?

I thought so, but I am beginning to change my mind.

> In what way does a SET of datatypes affect the
> BEHAVIOR of a
> piece of software? You do not specify any connection between datatypes and
> software. I think this needs to be spelled out a little more carefully
> (define it wrt a datatype API, maybe? )
>

Combining Pat's comments with Sandro's I now have a fairly different text
here.

I also add a paragraph about SHOULD NOT return Unknown and what is
"essential" that I will discuss in a separate thread.

Looking again at the definition of datatype theory in OWL S&AS (top of
section 3) it seems to be undefined for typed literals that are not in the
datatype theory, which was not adequately exposed in the OLD TEXT

OLD TEXT
[[
An OWL consistency checker takes a document as input, and outputs one word
being Consistent, Inconsistent, or Unknown.

An OWL consistency checker SHOULD report network errors occurring during the
computation of the imports closure.

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 datatypes supported
by its datatype theory [OWL Semantics and Abstract Syntax], if, given
sufficient (but finite) resources (CPU cycles and memory) and the absence of
network errors, it will always return either Consistent or Inconsistent;
otherwise it is complete. 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).

The datatype theory of an OWL consistency checker MUST minimally support at
least xsd:integer, xsd:string from [XML Schema Datatypes].

Five different conformance classes of OWL consistency checker are defined.

An OWL Lite consistency checker is an OWL consistency checker that takes an
OWL Lite document as input.

An OWL DL consistency checker is an OWL consistency checker that takes an
OWL DL document as input.

An OWL Full consistency checker is an OWL consistency checker that takes an
OWL Full document as input.

Note: Every OWL Full consistency checker is also an OWL DL consistency
checker. Every OWL DL consistency checker is also an OWL Lite consistency
checker. Every OWL Lite consistency checker can be trivially transformed
into an OWL Full consistency checker.

The different levels are intended to be used to indicate the intended domain
of a consistency checker.

Note: there are trivial implementations of these consistency checkers; for
example, one which always outputs Unknown.

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

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

Note: Complete OWL DL consistency checkers and Complete OWL Lite consistency
checkers MAY return Unknown on an OWL DL document or OWL Lite document in
the case where a resource limit has been exceeded.
]]

New Text:
[[
An OWL consistency checker takes a document as input, and *returns* one word
being Consistent, Inconsistent, or Unknown.

An OWL consistency checker SHOULD report network errors occurring during the
computation of the imports closure.

**
An OWL consistency checker MUST be <em>sound</em>: it MUST return
Consistent only when the input document is consistent and
Inconsistent only when the input document is not consistent.
**

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

**
An OWL consistency checker MUST NOT return Consistent when the input
document uses datatypes (other than in triples with predicate
owl:cardinality, owl:minCardinality and owl:maxCardinality) that are not
supported by the datatype theory of the consistency checker.
**

An OWL consistency checker is *decisive*, with respect to datatypes
supported by its datatype theory [OWL Semantics and Abstract Syntax], if,
given sufficient (but finite) resources (CPU cycles and memory) and the
absence of network errors, it will always return either Consistent or
Inconsistent,
**for an input document which only uses such datatypes**; otherwise it is
*indecisive*. It has been shown that for OWL Lite and DL it is possible to
construct a *decisive* consistency checker (the languages are decidable),
and that for OWL full it is not possible to construct a *decisive*
consistency checker (the language is undecidable) ** [Horrocks]. **

The datatype theory of an OWL consistency checker MUST minimally support at
least xsd:integer, xsd:string from [XML Schema Datatypes].

Five different conformance classes of OWL consistency checker are defined.

An OWL Lite consistency checker is an OWL consistency checker that takes an
OWL Lite document as input.

An OWL DL consistency checker is an OWL consistency checker that takes an
OWL DL document as input.

An OWL Full consistency checker is an OWL consistency checker that takes an
OWL Full document as input.

Note: Every OWL Full consistency checker is also an OWL DL consistency
checker. Every OWL DL consistency checker is also an OWL Lite consistency
checker.

--- Deleted sentence: Every OWL Lite consistency checker can be trivially
transformed into an OWL Full consistency checker. ---

The different levels are intended to be used to indicate the intended domain
of a consistency checker.

**
A consistency checker SHOULD NOT return Unknown. This requirement is to
remind implementors that Unknown, while sometimes needed, is not
a response desired by the user.
This requirement also clarifies that techniques
<link1>essential</link1> [Patent Policy] in non-trivial consistency
checkers are <link2>normative</link2> in this recommendation.
**

--- Delete note?
Note: there are trivial implementations of these consistency checkers; for
example, one which always outputs Unknown.
---

A *decisive* OWL Lite consistency checker is an OWL consistency checker that
is *decisive*.

A *decisive* OWL DL consistency checker is an OWL consistency checker that
is *decisive*.

Note: *Decisive* OWL DL consistency checkers and *decisive* OWL Lite
consistency checkers MAY return Unknown on an OWL DL document or OWL Lite
document in the case where a resource limit has been exceeded.
]]


The Horrocks paper is

[Horrocks et al., 1999] I. Horrocks, U. Sattler, and S. Tobies.
Practical reasoning for expressive description logics. In
Proc. of LPAR'99, vol. 1705 of LNAI, 1999.

(I need to look at this to check).



The <link1> to the definition of essential is:
http://www.w3.org/TR/2003/WD-patent-policy-20030319/#def-essential-definitio
n
and <link2> to
http://www.w3.org/TR/2003/WD-patent-policy-20030319/#def-essential-requireme
nts



Jeremy

Received on Tuesday, 13 May 2003 06:07:38 UTC