Re: comments on RDF MT

Pat,

Thank you for your response.

> In fact, the changes to the semantic conditions for subclass 
> and subproperty mean that the entire 'strategy' of the old proofs 
> is no longer tenable; the closure lemmas as stated are no longer true. 
> I have therefore gone back to a more traditional approach based directly 

> on Herbrand's theorem, which makes the proofs somewhat more elegant 
> in any case.

The new strategy you choose makes the proofs more elegant, I agree.
You added much new text in the proofs, together with many other changes
in the document, in a very short time.  I reread the proofs in the new
document from the beginning, and would like to point you to a few places 
where local adjustments in the new text are needed, in my view:

- Herbrand lemma.  Proof only if: Last part: ..., so Herb(E)<<I
instead of the other way around.
Proof if: the occurrences of [Herb(E)+A] and [I+A] need to be 
interchanged.
Or better: Suppose Herb E << I. Since Herb E satisfies E, there is 
a mapping A from the blank nodes of E so that I+A satisfies all triples 
from E, so I satisfies E.

- RDF closure lemma. Proof of the second semantic condition:
x is in HP iff <x, H(rdf:Property)> is in HEXT(H(rdf:type)):
The "only if" part ends with the conclusion that x is in HP,
which is not the expected end of an only if proof here.
I tried to construct the proof of this semantic condition for myself:

IF: suppose <x, H(rdf:Property)> is in HEXT(H(rdf:type)).
Then there must be a triple x rdf:type rdf:Property. in rdfclos(E).
Therefore x is in HP.

ONLY IF: suppose x is in HP. Then either x rdf:type rdf:Property. 
is in rdfclos(E) or s x o. is in rdfclos(E) for certain s and o.
In the latter case, the closure rules show that again,
x rdf:type rdf:Property. is in rdfclos(E). So in all cases,
<x, H(rdf:Property)> is in HEXT(H(rdf:type)).

Note that in this proof, I only use direct definitions, and do
not invoke the minimality of the Herbrand interpretation.


- Definition of Herbrand interpretation of G: IP is defined to be
..., or <as instead of a> subjects of triples ...

- The paragraph paragraph where separability is defined speaks about
E' separable from E.
The next paragraph speaks about 
E separable from G 
The next paragraph (Herbrand separation lemma) speaks about 
E' (not) separable from E.
These three paragraphs are strongly connected.  The middle paragraph gives 

E the role that E' has in the other paragraphs, while these other 
paragraphs
also contain E.  I found this confusing.  Suggestion: change notation in 
middle paragraph to E' sep. from E instead of E sep. from G.

Other comment about this middle paragraph: ... for some mapping from the
blank nodes of E to the <add: blank nodes and the> vocabulary of G, ...

- RDFS closure lemma sketch: the paragraph starting with "The first part 
follows from ..." pertains now to the RDFS entailment lemma instead.
Compare the first part of the proof of the RDF entailment lemma.


Best regards,

Herman ter Horst
Philips Research