Re: Process for editorial fixes? Re: Missing test:entailmentRules arcs (fwd)

>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