Re: comments on 26 September version of RDF Semantics document

>	Comments on RDF Semantics (version dated 26 September 2003)
>
>
>I did a quick read of the most of RDF Semantics, along with a careful
>investigation of a couple pieces.

Thanks.

>  Here are my comments.
>
>1/ The major new issue I have with the document is the unsupported change
>of the entailment rules from informative to normative.

Just for the record, that change happened a few versions ago; but 
your comment is noted.

>
>2/ The removal of the translation to LBase is a major improvement.  I would
>have prefered different wording in Section 0.1 concerning this translation
>but can live with the new situation.
>
>3/ The document is of several minds with respect to just what the semantics
>of RDF (and RDFS) is.  There is wording in Section 1.3 to the effect that
>the definition of the semantics of RDF and RDFS excludes the entailment
>rules.  How can this coexist with having the entailment rules be normative?

Well, the rules are not part of the semantics as such. The issue of 
their normativeness (normativity? normitude?) seems to be orthogonal 
to this point. The Abstract of the document begins

"This is a specification of a precise semantics, and corresponding 
complete systems of inference rules, for...."

clearly indicating that the semantics is one thing, and the rules 
another, a division reflected in the organization of the document.

(??Maybe I havnt followed your point here??)

>
>4/ The figures in the copy of the document that I reviewed have naming
>problems, but I am told that these have since been fixed.

They may not have been fixed to your satisfaction. The changes were 
largely graphical (color, font rendering) rather than textual. We 
have discussed the issue of the wording in figure 1, and I responded 
in an earlier message.

>
>5/ The Monotonicity and Compactness Lemmas are only stated for simple
>entailment.  However, readers could easily be left with the impression that
>the other forms of entailment could also have the desirable properties that
>accrue from these lemmas.

The text states explicitly:

"These results apply only to simple entailment, not to the extended 
notions of entailment introduced in later sections."

reiterated after the statement of the anonymity lemma:

"Note again that this applies only to simple entailment, not to the 
vocabulary entailment relationships defined in rest of the document.".

Later, when RDF-entailment is introduced (section 3.1, second 
paragraph) the document repeats the warning, with a back-link and an 
illustrative example.:

"It is easy to see that the lemmas in <a href>Section 2</a> do not 
all apply to rdf-entailment: for example..."

I think this constitutes an adequate safeguard against this misunderstanding.

>
>6/ The characterization of simple entailment rules is misleading as they do
>not currently correspond to the instance lemma.  The comment on how to make
>this change at the end of Section 7.1 does not adequately serve to correct
>the misimpression.

Let me suggest a re-wording and expansion of the first line of 
section 7.1 as follows. Would this be more acceptable?

"The interpolation lemma in section 2 characterizes simple entailment 
in terms of instances and subgraphs. Being a subgraph requires no 
explicit formulation as an inference rule on triples, but one can 
give rules which generate generalizations, for example: "

>7/ The document needs a better description of consistency and
>inconsistency.

Can you elaborate? Ah, I see that there is no glossary entry for 
'consistent'; I will rectify this.

>
>8/ The change to the RDFS entailment lemma is incorrectly noted in the
>change log as editorial.

It was considered editorial because it was considered to be a 
correction of an error in the text rather than a change to the lemma.

>9/ I view the development and statement of the entailment lemmas as
>fundamentally flawed.  I look for soundness and completeness in any such
>syntactic characterization of entailment.  Neither simple entailment, RDF
>entailment, nor RDFS entailment have both these characteristics.

In the sense of 'complete' you probably mean, that is correct. They 
never have been written in that style and I see no useful purpose to 
be served by so doing.

>9a/ Section 7.1 does not provide any statement at all on whether the simple
>entailment rules are complete with respect to simple entailment.

Section 2 has already noted, however :

"The interpolation lemma completely characterizes simple RDF 
entailment in syntactic terms. To tell whether a set of RDF graphs 
entails another, check that there is some instance of the entailed 
graph which is a subset of the merge of the original set of graphs. 
Of course, there is no need to actually construct the merge. If 
working backwards from the consequent E, an efficient technique ..."

followed by a paragraph of discussion. The amended text (above) at 
the beginning of section 7.1 will refer back to this.

I also note that section 7 begins by saying :

"The following tables list some inference patterns which capture some 
of the various forms of vocabulary entailment."

and does not refer to simple entailment. As you may recall, the 
inference rules in section 7.1 were introduced in order to ensure 
that the RDF and RDFS closures included appropriate generalizations 
of some of the entailed triples.

>There is
>a statement that the rules are sound, and that an agumentation of them
>correspond to the instance lemma, but no proof is presented.

That is true; however, I do not think that a proof is needed, as the 
relevant syntactic condition is fully described by the interpolation 
lemma.

To provide a complete set of rules which implement the relevant 
search as a forward application of valid entailment rules would be 
computationally ridiculous. Since the main purpose of describing 
entailment rules in this document is not as an exercise in textbook 
formal logic, but rather to provide a useful guide to suggest 
relatively easy implementation styles for inference engines, to adopt 
the style you are here suggesting in the main body of the document 
would in my view serve no useful purpose and would likely be 
counterproductive.

However, I plan to insert the following in the proof appendix (just 
after the QED of the interpolation lemma) , with a forward link from 
section 7.1 (end), which may go some way towards satisfying your 
point. (This change has not yet been discussed by the WG. )

---------
This lemma can be used as the basis for several different mechanical 
processes for checking simple entailment. One way to characterize 
entailment syntactically is in terms of inference rules which apply 
to a set S and can be used to derive E just when S entails E. For 
example, a slight modification of the simple entailment rules 
described in section 7.1 will suffice, where we allow new blank nodes 
to be allocated to existing blank nodes as well as to URI references 
and literals:

extended simple entailment rules.
---------<table>------
Rule name

If E contains

then add

xse1

uuu aaa xxx .

uuu aaa _:nnn .

where _:nnn is a blank node identifier allocated to xxx by rule xse1 or xse2.

xse2

uuu aaa xxx .

_:nnn aaa xxx .

where _:nnn is a blank node identifier allocated to uuu by rule xse1 or xse2.
----------</table>--------
These rules allow blank nodes to proliferate, producing highly 
non-lean graphs; they sanction entailments such as

ex:a exp ex:b .
ex:a ex:p _:x . by xse1 with _:x allocated to ex:b
ex:a ex:p _:y . by xse1 with _:y allocated to _:x
_:z ex:p _:y . by xse2 with _:z allocated to ex:a
_:u ex:p _:y . by xse2 with _:u allocated to _:z
_:u ex:p _:v . by xse1 with _:v allocated to _:y

It is easy to see that if S is an instance of T then one can derive T 
from S by applying these rules in a suitable sequence; the rule 
applications required can be discovered by examination of the 
instance mapping. So, by the interpolation lemma, S entails E iff one 
can derive (a graph containing) E from S by the application of these 
rules. However, it is also clear that applying these rules naively 
would not result in an efficient search process, since the rules will 
not terminate and can produce arbitrarily many redundant derivations 
of equivalent triples.

The general problem of determining simple entailment between 
arbitrary RDF graphs is decideable but NP-complete. This can be shown 
by encoding the problem of detecting a subgraph of an arbitrary 
directed graph as an RDF entailment, using blank nodes to represent 
the graph (observation due to Jeremy Carroll.)
-----------


>
>SUGGESTION:  I suggest that Section 7.1 be augmented with the following
>Lemma and that its proof be added to Appendix A.
>
>	Simple entailment lemma. S simple-entails E iff there is a graph
>	that can be derived from S by the application of the simple
>	entailment rules that is a supergraph of E.  (Proof in Appendix A.)
>This lemma requires that the simple entailment rules be augmented to allow
>vvv in rule se1 and bbb in rule se2 to be a blank node.

See above.

>
>9b/ Section 7.2 does not provide an adequate syntactic characterization of
>RDF entailment.
>
>SUGGESTION:  I suggest that Section 7.2 be augmented by the following
>change to the RDF entailment lemma and that its proof in Appendix A be
>modified accordingly.
>
>	RDF entailment lemma.  S rdf-entails E if and only if ... and which
>	is a supergraph of E.  (Proof in Appendix A.)
>
>
>9c/ Section 7.3 does not provide an adequate syntactic characterization of
>RDF entailment.
>
>SUGGESTION:  I suggest that Section 7.3 be augmented by adding the
>following lemma and providing a proof for it in Appendix A.
>
>	RDFS consistency lemma.  S is rdfs-consistent if and only if it is
>	not possible to derive a supergraph of a graph of the following
>	form from S plus the RDF and RDFS axiomatic triples by the
>	application of the simple, RDF, and RDFS entailment rules
>
>		uuu vvv rrr^^rdfs:XMLLiteral .
>		vvv rdfs:range www .
>		www rdfs:subClassOf rdfs:Literal .
>
>	where rrr is a non-well formed XML literal.  (Proof in Appendix A.)
>
>I believe that this is a correct characterization of RDFS consistency but
>this would have to be shown in the proof.
>
>SUGGESTION:  I suggest that Section 7.3 be augmented by the following
>change to the RDFS entailment lemma and that its proof in Appendix A be
>modified accordingly.
>
>	RDFS entailment lemma.  If S is rdfs-consistent then S rdfs-entails
>	E if and only if ... and which is a supergraph of E.  (Proof in
>	Appendix A.)

Thanks for your suggestions.

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 Monday, 29 September 2003 13:17:11 UTC