Re: LC2 semantics proof appendix

From: pat hayes <phayes@ihmc.us>
Subject: LC2 semantics proof appendix
Date: Thu, 9 Oct 2003 22:41:25 -0500

> 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.

Consider the RDF graph

	ex:foo rdf:type rdf:Property .

The Herbrand interpretation, H, for this is then

	IRH = { ex:foo, rdf:Property } u LVH
	IPH = { ex:foo, rdf:type }
	IEXTH(rdf:type) = { <ex:foo,rdf:Property> }
	IEXTH{x) = {} otherwise
	ISH = id
	ILH = id
	LVH = strings u pairs

What I would consider to be the minimal interpretation, M, is

	IRM = { ex:foo, rdf:Property } u LVM
	IPM = { rdf:type }
	IEXTM(rdf:type) = { <ex:foo,rdf:Property> }
	IEXTM{x) = {} otherwise
	ISM = id
	ILM = id
	LVM = strings u pairs

I do not believe that H << M.

Ignoring strings and pairs (where the mapping is identity) the projection
mapping is going to have to look like

	k(rdf:Property) = rdf:Property	because ex:foo is the only object
	k(rdf:type)	= rdf:type	because rdf:type is the only predicate
	k(ex:foo)	= ex:foo	because ex:foo is the only subject

but then ex:foo is in IPH and k(ex:foo) is not in IPM.
   
By the way, the IL mapping of typed literals in Herbrand interpretations is
broken.  It is defined to be the identity mapping but LV only contains
string, pairs of strings and language tags, and well-formed XML literals in
G.  What then is IL("foo"^ex:bar)?

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




peter

Received on Friday, 10 October 2003 06:17:48 UTC