Re: datatyping in test for Pat's review

(Sending this quickly, more comments later.  -Pat )

section 4.1.2.
model/satisfying interpretation (Neither the RDF nor OWL documents 
uses 'model' in this technical sense.)

2nd 'consistent' is potentially misused (referring to an 
interpretation), suggest
consistent with the constraints ... /satisfies all the constraints ....

4.2.2
Im still not happy with the way that conformance is stated.

Discussion. The problem is that 'complete' means something different 
when applied to inconsistency and consistency checking.  OK, you 
don't want to have two kinds of conformance, but there must be a way 
to get this stated which isn't so misleading.

Here is the standard account. An inconsistency checker is complete 
if, given any inconsistent input, it will eventually return 
'Inconsistent'. That is the standard definition of 'complete' used 
ever since Goedel's first theorem and throughout the logical 
literature, the sense in which resolution is complete and FOL has a 
complete proof theory. The analogous statement for consistency is 
false in these cases, because the task of determining consistency is 
one recursion class higher than for inconsistency, in general (so 
following your definition, and the observation that inconsistency of 
(A and not B) is the same as A entailing B,  would lead to the 
assertion that there was no complete inference system for first-order 
logic, for example, which sounds like a denial of the central theorem 
of FOL proved by Goedel in 1938.)  However, for subcases which are 
*decideable* - such as DLs - then termination of a complete 
inconsistency checker without finding inconsistency amounts to 
determining consistency. That is, you can in effect use 
negation-by-failure reasoning when you know (1) it is complete and 
(2) we know the problem is decideable.

The trouble with your 'complete and terminating' phrase is that it is 
natural to read this is a conjunction of two properties, viz. 
complete and terminating, and then to ask what it be to be complete 
and non-terminating.  Since the sense of 'complete' that you use only 
lines up with the standard notion in the case where it is 
terminating, there is a constant danger of this being misread as 
meaning exactly what it seems to say, rather than your meaning.

The cheapest way around this would be to add a remark when you give 
the definition of 'complete' to indicate that this sense is not the 
standard sense. For example
"This is stronger than the usual sense of completeness used in 
describing logical inference systems, which refers only to the 
detection of inconsistency."

A better way, IMHO, would be to use a different term. How about 
'decideable', would that be less likely to stick in Ian's craw? It is 
slightly nonstandard (the word is usually applied to the problem than 
to the algorithm) but clear in its meaning, fits well onto the useage 
for the DL case (on a decideable subcase, a complete correct 
algorithm is a decision procedure) and fits naturally: one can have a 
decideable consistency checker just when the problem  of deciding 
consistency is a decideable problem. This has the merit of not 
mis-using an established terminology in a misleading way, it uses a 
conventional word, and it is shorter than "complete and terminating".

My preference would be to use 'decideable' (or any word or phrase 
that does not misuse the word 'complete') and be (reluctantly) 
willing to go with the current wording but only if it is protected at 
the point of definition (6th para of 4.2.2) with a suitable warning.


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

Received on Saturday, 17 May 2003 11:58:04 UTC