- From: pat hayes <phayes@ihmc.us>
- Date: Fri, 7 Nov 2003 18:13:37 -0600
- To: Brian McBride <bwm@hplb.hpl.hp.com>
- Cc: w3c-rdfcore-wg@w3.org
>Jan Grant wrote: >>Incidentally, should I be making editorial fixes to a particular copy of >>the document now? > >The process we specified was that editors circulate proposed changes >and the chairs decide whether they are editorial or require WG time >to discuss. Ah. Then I have been remiss. Summary of changes to semantics since LC2: 1. Proof appendix totally rewritten (the LC2 version was known to be buggy and had explicit disclaimers on these proofs.) The effect is to do away with a lot of definitions that were causing more harm than good (notably the notion of subderivation) and showing that the 'big' proofs are now explicitly modelled on the basic Herbrand proof. Interestingly, nearly all the extra complication arises from XML literals. 2. Simple entailment rules now generate all possible generalizations (so are complete, as Peter wanted, but impractical, as noted) 3. New special-case rule 'lg' added for use in the subsequent entailment lemmas: this just generates one new bnode per literal. BTW, if an API allows type information to be attached to literals (ie if literals can be, nudge nudge, wink, 'subjects') then that's all that is really needed: the only reason for having rule lg is to provide a bnode surrogate for every literal, which of course can be a subject. Once that's done you can forget the literals altogether and just use the bnode: or, of course, you can identify them. I'm not allowed to do that in legal RDF so I have to use lg as a work-around. The 'sur' construction in the proof of the RDFS entailment lemma makes it all clear.) 4. Rules referring to literals (rdf2, rdfs1, rdfD1) now all refer to rule lg, and add triples without generating new bnodes. 5. A way of recognizing RDFS inconsistencies is described (called an XML clash, by analogy with datatype clash) and incorporated into the statement of the RDFS entailment lemma. (2-5 all arose from insights obtained by writing out the appendix proofs in full, which I ought to have done long ago, of course....) 6. Section 7 has been revamped so that the same uuu/vvv/xxx/yyy conventions are used in all the rules and examples: there were bugs and patches in this before. Rules rdfs 5 and 9 had mistaken restrictions in them, noted by Herman, which are now fixed (subjects can be bnodes as well as URIs). (All of the above is to non-normative text.) 7. The definition of 'vocabulary of a graph' (section 0.3) has been simplified: it is just the names on the nodes and arcs of the graph. This is a long-overdue simplification which makes no difference to anything except the wording of the proofs and tossing out some confusing definitions that aren't needed (like name IN graph vs. name FROM graph). Thanks to Herman for chewing on the IN/FROM distinction until I was obliged to fix it. 8. (related). The definitions of rdf and rdfs entailment have been simplified so that they do not make explicit reference to a vocabulary. This is actually more conventional; and Herman pointed out that the more complicated definitions meant that entailment might not be transitive (aargh). The motive for introducing this complication in the definition in the first place has been removed by subsequent changes. This doesn't change any test cases. 9. Several pieces of explanatory prose have been added here and there, in some cases just to make notational conventions more evident, in others to draw attention to places where some point is relevant or to give an intuitive justification for a formal definition. All of these have been motivated by comments, mostly by Herman, though also in some cases by folk at ISWC. 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 Friday, 7 November 2003 19:16:05 UTC