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

Re: LC2 semantics proof appendix

From: pat hayes <phayes@ihmc.us>
Date: Fri, 31 Oct 2003 16:31:14 -0600
Message-Id: <p06001f1cbbc881e6aaf7@[10.1.31.1]>
To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
Cc: herman.ter.horst@philips.com, w3c-rdfcore-wg@w3.org

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

Sorry.

The change has indeed been rescinded
http://www.w3.org/2001/sw/RDFCore/TR/WD-rdf-mt-20030117/#defherbinterp
; but more importantly, the subinterpretation 
relationship << is no longer used in the proof 
and is not defined anywhere, so this issue is no 
longer germane to any of the lemmas. The previous 
exposition has been simplified into a single proof
http://www.w3.org/2001/sw/RDFCore/TR/WD-rdf-mt-20030117/#interplemmaprf
using the Herbrand construction to prove the 
interpolation lemma directly. This contracts what 
was three lemmas (one of which was so trivial 
that you considered it to be circular) into a 
single argument and removes the need for the << 
construction and the explicit notion of 
minimality.

The longer proofs of the entailment lemmas are 
then modelled on this construction and argument, 
with suitable modifications and notational 
extensions (mostly needed to handle literals.)

Pat


>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


-- 
---------------------------------------------------------------------
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, 31 October 2003 17:34:43 EST

This archive was generated by hypermail pre-2.1.9 : Friday, 31 October 2003 17:34:48 EST