comments on OWL test cases

I'm looking at  http://www.w3.org/2002/03owlt/editors-draft/draft/ dated 12 May

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.

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?

The terminology "complete" here is unfortunate as it is in conflict 
with established usage of this term in logic. I would suggest either 
using this term in conformance with its standard usage, or else use a 
different term.

In fact, I would suggest a more thorough rewriting of this section. 
(I am willing to draft an alternative if that would be helpful. ) 
[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.] It is written in a style which suggests, potentially 
misleadingly, that consistency and inconsistency checking are 
somewhat symmetrical, or even two aspects of one problem. In fact, 
they are sharply different in complexity for most languages, and 
inconsistency detection - but not consistency detection - is closely 
related to entailment. 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.

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.

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

The final NOTE in this section refers only to DL and Lite: why? This 
is characteristic of all forms of completeness.

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.

The English gloss on some of the tests (eg 
http://www.w3.org/2002/03owlt/editors-draft/draft/byFunction#function-FunctionalProperty
refers to 'arcs', which is a term that is now deprecated by the RDF 
WG.  Might this be better phrased? Example:

If prop belongs to owl:FunctionalProperty , and subject denotes a 
resource and has two outgoing prop arcs, then the object s of these 
arcs  have the same denotation. Hence an arc originating in object1 
can be copied to object2 .
/
If prop belongs to owl:FunctionalProperty , and subject denotes a 
resource which is the subject of two prop triples, then the object s 
of these triples have the same denotation. Hence any assertion made 
using one of them can be transferred to the other.

In general, perform substitutions
'has FOO incoming prop arc' /'is the object of FOO prop triples'
'has FOO outgoing prop arc' /'is the subject of FOO prop triples'

No other complaints. Full marks on layout, overall document 
structure, etc., and extra credit for C.5.1 :-)

Pat

PS. The Ntriples turquoise background looks rather dark and menacing 
on my screen. Somewhere closer to #c0e0e0, maybe?
-- 
---------------------------------------------------------------------
IHMC					(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola              			(850)202 4440   fax
FL 32501           				(850)291 0667    cell
phayes@ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam@ai.uwf.edu   for spam