- From: <herman.ter.horst@philips.com>
- Date: Tue, 12 Nov 2002 16:06:26 +0100
- To: pat hayes <phayes@ai.uwf.edu>
- Cc: www-rdf-comments@w3.org
- Message-ID: <OF192F1D2C.6C93E9A6-ONC1256C6F.004CB6F7-C1256C6F.00532F54@diamond.philips.com>

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

Received on Tuesday, 12 November 2002 10:40:25 UTC