From: <herman.ter.horst@philips.com>

Date: Thu, 6 Nov 2003 19:19:29 +0100

To: pat hayes <phayes@ihmc.us>, www-rdf-comments@w3.org

Message-ID: <OFDCF011BC.B1ADB556-ONC1256DD6.0053CE23-C1256DD6.0064BAB2@diamond.philips.com>

Date: Thu, 6 Nov 2003 19:19:29 +0100

To: pat hayes <phayes@ihmc.us>, www-rdf-comments@w3.org

Message-ID: <OFDCF011BC.B1ADB556-ONC1256DD6.0053CE23-C1256DD6.0064BAB2@diamond.philips.com>

This is a review of part of the RDF Semantics document, editorial version LC2.5. In this message I mainly focus on the rdfs entailment lemma. The proof of this lemma is based on the claim that the RDFS Herbrand interpretation of an RDF graph is an RDFS interpretation. This claim seems to be false: the first condition for RDF interpretations is not satisfied. In order to show this, note that this condition amounts, in this case, to the equivalence v in IP iff <v,Property> in IEXT(type). Suppose that the graph G has triples v p l and p range Property where l is a plain literal. By rule lg, the RDFS closure D of G contains the triple v p b where b is allocated to l and where b = sur(l). By rule rdfs3, D contains the triple b type Property = sur(l) type Property. Therefore, <l,Property> in IEXT(type). However, we cannot have l in IP, since that would mean that D contains the triple l type Property. === It should be made explicit what the domain and range of the function sur are: I assume that these sets are both IR. When this assumption is made explicit, there seems to be a circularity in the definition of LV for the RDFS Herbrand interpretation: the definition of LV depends on sur, the definition of sur depends on IR, the definition of IR depends on LV. In view of this circularity, the definition of LV becomes incomprehensible. I believe that the definition of LV should be made explicit. From the given definition, I would guess that the intention is that LV is the union of five sets: strings pairs of strings and language tags XML values of well-typed XML literals in D {v in voc(D): the triple v type Literal is in D } {v in voc(D): v a typed, non-XML literal such that b type Literal is in D, where b is the blank node allocated to v by rule lg } === "Define B(x) as before, then clearly [SH+B] satisfies D ..." There seems to be a problem with this conclusion. Making this explicit, it seems that B:blank(D)->IR needs to be defined by B(v)=xml(l) if v is a blank node allocated to the well-formed XML literal l, B(v)=l if v is a blank node allocated to a typed, non-XML literal l, otherwise B(v)=v. (The second case is not exactly as before, but seems to be needed to develop a complete proof of the condition LV = ICEXT(Literal).) Given a triple vpw in D, rule rdf1 shows that D contains the triple p type Property so that p in IP. In order to prove that SH+B satisfies vpw, i.e. that <SH+B(v),SH+B(w)> in IE(p), it is sufficient to prove that D contains the triple * sur(SH+B(v) p sur(SH+B(w)). Note that sur(SH+B(v)) = v (when v in nodes(D) - literals) sur(SH+B(v)) = b (when b is the blank node allocated to v in nodes(D) intersection literals) (this can be checked for each of many different cases). So it can be concluded that D contains the triple * when lg can be applied in each step of the construction of D. However, rule lg is only used as the first step. It seems that this problem would be solved when rule lg can always be used in the construction of D === There seem to be problems with the proof of the condition IR = ICEXT(Resource). It only needs to be proved that if x is in IR, then <x,Resource> in IE(type>, as the opposite is trivial. (Note that the document states the opposite. Note also that for the proof of LV=ICEXT(Literal), the document only states an if statement instead of an two statements.) However, there are many cases. The proof is not clear. It seems that the proof uses and needs to use the triple ** Literal subClassOf Resource, which however is not an axiomatic triple, to my surprise. Shouldn't this triple ** be made into an axiomatic triple? The last lines of the four proof parts consist of the triple x type Resource If x is a URI this suffices to prove that <x,Resource> in IE(type>, however when x is a blank node or a literal this is not sufficient. === Herman ter HorstReceived on Thursday, 6 November 2003 13:20:21 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:15:21 UTC
*