Re: dissatisfaction with the entailment rules development

>I am deeply dissatisfied with the way the various entailment rules are
>specified in the RDF Semantics document (currently the version of 31 July).
>I had hoped that the entailment rules would finally end up as complete
>syntactic characterizations of entailment.

As the text says, and has always been the case through all versions 
of the document, the rules characterize vocabulary entailments by 
'reducing' them to simple entailment. Simple entailment is fully 
captured by the interpolation lemma in section 2.

Your dissatisfaction, and its depth, is noted, although I have not 
yet fully grasped the reasons for it. However, you seem to be alone 
in this particular dissatisfaction; and since the overall design of 
the entire document is, and always has been, largely dependent on 
this distinction between (methods for determining) vocabulary 
entailment being reducible to (methods for determining) simple 
entailment, I do not propose to alter it at this stage.  I do not 
think it would be useful or appropriate to give logically complete 
inference rules for simple entailment as an implementation would 
likely be based on unification rather than existential generalization 
in any case. Unification applied to RDF is likely to blend together 
subgraph and instantiation operations, so I did not (and do not) feel 
that it is useful to keep them as separate inference rules when 
discussing a graph syntax.

I also note that these lemmas have always been stated in this style 
(ie in terms of a reduction, by use of rules, to a case of simple 
entailment), consistently, ever since the first draft of the document 
was written, and that you have had ample opportunity to note this and 
object to it previously. They have never been intended to be strongly 
complete; until recently, they were described as 'closure rules' to 
emphasize this point.

>  This would result in lemmas
>somewhat along the following lines:
>
>RDF(S) entailment lemma:  S rdf(s)-entails E if and only if there is a
>graph that can be derived from S plus the RDF (and RDFS) axiomatic triples
>by the appliation of the simple entailment rules and RDF entailment rules
>(and RDFS entailment rules) which is a supergraph of E.
>
>Instead the entailment lemmas are incomplete in a disturbing way.

I am not sure what you mean by 'incomplete'. The lemmas are, I 
believe, correct as stated. I do not find weak completeness 
disturbing; very few, if any, mechanical inference systems are 
strongly complete, for example.

>The RDF
>entailment lemma defers to simple entailment, which makes it an incomplete
>characterization of rdf-entailment.  It would be much better to remove this
>incompleteness.

I do not accept that it is 'incomplete', and I disagree that it would 
be 'better' to modify it along the lines you sketch above. The 
current way of stating the lemmas was chosen deliberately, in part to 
distinguish the part of the entailment that is due to graph 
operations from that which is dependent on a particular vocabulary.

>The RDFS entailment lemma also depends on simple entailment, but also has a
>condition that S be rdfs-consistent.

If it was possible for a graph to be rdf-inconsistent, then there 
would be a similar condition in the statement of the other lemma.

These rules are not fully logically complete, and have never been 
claimed or intended to be. Such a set of rules would contain all kind 
of redundant inferences.  (It would be nice if one could give rules 
which would reduce an inconsistency to some standard 'inconsistency 
marker' such as a null clause, but RDF has no such marker so I did 
not attempt to write such rules.)

>This detracts considerably from the
>utility of the RDFS entailment rules.

I disagree. A fully complete set of rules would be of considerably 
less utility.

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@ihmc.us       http://www.ihmc.us/users/phayes

Received on Tuesday, 5 August 2003 12:28:24 UTC