W3C home > Mailing lists > Public > w3c-rdfcore-wg@w3.org > October 2003

LC2 semantics proof appendix

From: pat hayes <phayes@ihmc.us>
Date: Thu, 9 Oct 2003 22:41:25 -0500
Message-Id: <p06001f21bbabd3a9edc0@[10.0.100.25]>
To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, Herman terHorst <herman.ter.horst@philips.com>
Cc: w3c-rdfcore-wg@w3.org

Guys, in case you plan to review the appendix in the LC version of 
the semantics document, I ought to tell you that I was mortified to 
found a huge bug in the proofs of the RDF and RDFS entailment lemmas 
just hours before the publication deadline, and had to do some very 
hasty repair work, so the proofs in the published version are 
extremely ugly and seriously incomplete. Frankly, the RDFS lemma 
proof is not worth the bother of trying to review - it is a 
placeholder - so please feel free to ignore them other than to say 
they are trash. I am writing up a better version which I will send 
you as soon as it is ready, early next week. That will, I hope, 
include a version of the RDFS consistency lemma which Peter has 
suggested.

Pat

PS. You may notice that I have restored a condition on IP in Herbrand 
interpretations which you suggested earlier that I remove. I had 
forgotten that this condition, although inelegant, is necessary in 
order to handle the case of the RDF lemma when the graph contains a 
triple

aaa type Property .

but aaa is not used as a property. In this case, with the 'standard' 
definition of IP in a Herbrand interpretation being just the set of 
property URIrefs, the construction used in the RDF lemma fails, since 
the RDF interpretation requires that IP be exactly the class 
extension of rdf:Property.  Adding these URIs to IP makes no extra 
triples true, so does not affect the minimality of the Herbrand 
interpretation, and is harmless for the other (elementary) Herbrand 
results, so I have restored this condition. Just to let you know that 
I didn't do so carelessly or on a whim.

The basic reason for this being necessary is that RDF allows 
properties to exist which have an empty extension, by the way.

-- 
---------------------------------------------------------------------
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 Thursday, 9 October 2003 23:44:23 EDT

This archive was generated by hypermail pre-2.1.9 : Thursday, 9 October 2003 23:44:28 EDT