Re: model theory publication draft

At 02:27 PM 9/18/01 -0500, Pat Hayes wrote:
>At last the model theory is in readable form, at
>
>http://www.coginst.uwf.edu/~phayes/RDF%20MT-currentdraft.html

Pat,

I have a couple of small comments/questions about this, and a more 
substantial issue (the final point below).


- the document variously uses the terms URI, uriref, <uriref> to mean 
something like "URI-plus-optional-fragment".  Maybe we could coin a term 
for this and use it consistently?


- Section 5:
I thought this was great;  very neat.  Would I be correct in thinking that 
the schema-closure of any graph satisfies the Strong Herbrand Lemma.

Hmmm.. as stated, I think this is trivially true, as the lemma is stated in 
terms of satisfaction, which is not affected by the new inferences based on 
schema constructs.  I think what I want to suggest is this version of the 
lemma:
   The schema-closure of any RDF graph has an RDFS interpretation that 
satisfies the graph and does not satisfy any ground triple not in the graph.


 >>> the substantial issue:

- Section 5:
I think there may be a problem with the schema lemma, in { S1, S2 } entails E:

S1:  x:a rdfs:subClassOf x:b .

S2:  x:b rdfs:subClassOf x:c .

E:   x:a rdfs:subClassOf x:c .

Schema closures:

S1:  x:a             rdfs:subClassOf x:b .
      rdfs:subClassOf rdf:type        rdf:Property .
      rdf:type        rdf:type        rdf:Property .
      rdf:Property    rdf:type        rdfs:Class .
      rdf:Property    rdfs:subClassOf rdfs:Resource .
      rdfs:Class      rdf:type        rdfs:Class .
      rdfs:Class      rdfs:subClassOf rdfs:Resource .
      rdfs:Resource   rdf:type        rdfs:Class .
      rdf:type        rdf:type        rdfs:Resource .
      rdfs:Class      rdf:type        rdfs:Resource .
       :
      (+ others not including x:a or x:b)

S2:  x:a             rdfs:subClassOf x:b .
      rdfs:subClassOf rdf:type        rdf:Property .
      rdf:type        rdf:type        rdf:Property .
      rdf:Property    rdf:type        rdfs:Class .
      rdf:Property    rdfs:subClassOf rdfs:Resource .
      rdfs:Class      rdf:type        rdfs:Class .
      rdfs:Class      rdfs:subClassOf rdfs:Resource .
      rdfs:Resource   rdf:type        rdfs:Class .
      rdf:type        rdf:type        rdfs:Resource .
      rdfs:Class      rdf:type        rdfs:Resource .
       :
      (+ others not including x:a or x:b)

Applying the interpolation lemma, the merge of s-closure(S1) and 
s-closure(S2) does not contain E as a subgraph.  But, intuitively S1 and S2 
together should entail E.

The problem, I think, is that the schema closure is applied before doing 
the graph merge.  I think the lemma should be something like this:

   S s-entails E iff the schema-closure of the merge of members of S entails E.

#g


------------------------------------------------------------
Graham Klyne                    MIMEsweeper Group
Strategic Research              <http://www.mimesweeper.com>
<Graham.Klyne@MIMEsweeper.com>
------------------------------------------------------------

Received on Wednesday, 19 September 2001 13:22:36 UTC