Re: LC2 semantics proof appendix

I have not received any response to this comment on the change to Herbrand
interpretations.  (This change may have been rescinded but I would like
some indication thereof.)

peter


From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
Subject: Re: LC2 semantics proof appendix
Date: Fri, 10 Oct 2003 06:17:31 -0400 (EDT)

> 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, 31 October 2003 11:52:11 UTC