semantics proof appendix fixed

There is a version of the LC2 Semantics document with @@ in its date line at

http://www.ihmc.us/users/phayes/RDF_Semantics_LC2.4.html

which finally has a readable proof appendix.

It also has an improved version of the entailment rules. The 
'closures' for RDF and RDFS now use only a very restricted form of 
the simple entailment rules which apply only to literal objects (as 
you will see in the proof, for RDF one only needs to use this on 
well-formed XML literals, in fact) and all the subsequent similar 
rules (rdf2, rdfs1, rdfD1) are linked to this rule, so that the 
closures only generalize in a very restricted way so as to, in 
effect, provide unique blank-node surrogates for literals, which is 
sufficient for completeness. The results given here still apply to 
the older rules, since those generate all these conclusions and more, 
but the rules given here are leaner and meaner.  Jos and Graham, if 
you check out the definition of rdf-closure in the proofs, you will 
get an even leaner and meaner RDF version.

The only change to any normative text is a fix to a bug which I found 
in the RDFS semantic condition for rdfs:Datatype, which had not been 
brought up-to-date after the intensional subClass changes made a 
while ago (it referred to rdf:type rather than rdfs:subClassOf). The 
change is invisible to any extensional extension so does not affect 
OWL.

Eric and Brian: this passes all the filters I can test it on, except 
for the deliberately broken 'this version' link with @@ in the date

Apologies again for this work missing the LC2 deadline.

Eric, no doubt it is impossible for various reasons, but if the 10/10 
semantics URL could be redirected to this document instead of the one 
you put up on Friday, then there might be a lot of people out there 
who might be saved a lot of useless reading.  It is 
XHTML/CSS/link/anchor OK, but the boilerplate might want checking for 
pubrules.

Peter and Herman, I would be grateful for your views on the proofs 
(and for your NOT reviewing the version put out last Friday, to my 
mortification.)

You will be relieved to see that I have completely abandoned the 
proof strategy involving subinterpretations, and instead proven the 
interpolation lemma directly using a mapping from the Herbrand 
interpretation, and then modelled the longer proofs on this by 
modifying the Herbrand interpretations suitably. Most of the work is 
now concerned with literals, and the proofs actually provide, I 
think, some useful insight into how literal generalization can be 
handled in a reasoner.  The RDFS proof is given in full, although in 
a compact form.

Peter, re. your complaint about the 'style' of the entailment lemmas, 
I still prefer this overall way of stating the lemmas in terms of a 
reduction to simple entailment, as it provides a more detailed 
insight into what one might call the proof theory.  However, many of 
the issues you pointed to have been dealt with.  I have put the full 
version of se1 and 2 into the main text, so that the simple 
entailment rules do indeed fully capture simple entailment; and the 
RDFS entailment lemma now covers the case where the antecedent is 
rdfs-inconsistent. I hope you will agree that the 'XML clash' 
criterion is preferable to the rebarbative subgraph used previously.

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 Monday, 13 October 2003 15:04:04 UTC