- From: Graham Klyne <gk@ninebynine.org>
- Date: Thu, 31 Jul 2003 10:37:10 +0100
- To: Brian McBride <bwm@hplb.hpl.hp.com>
- Cc: pat hayes <phayes@ihmc.us>, rdf core <w3c-rdfcore-wg@w3.org>
At 10:10 31/07/03 +0100, Brian McBride wrote:
>On Wed, 2003-07-30 at 21:47, Graham Klyne wrote:
>
>[...]
>
> >
> > Then I( ppp rdf:type rdf:Property ) is true, which is the desired
> entailment.
>
>False. I(ppp rdf:type rdf:Resource) was the test case.
Rats! I knew that, really!
Given the truth (from before) of:
(1) I( ppp rdf:type rdf:Property )
and the axiomatic triple:
(2) rdf:type rdfs:domain rdfs:Resource .
-- http://www.w3.org/2001/sw/RDFCore/TR/WD-rdf-mt-20030117/#rdfs_interp
and:
(3) if E is a triple s p o . then I(E) = true if
s, p and o are in V, I(p) is in IP and <I(s),I(o)> is in IEXT(I(p))
otherwise I(E)= false.
-- http://www.w3.org/2001/sw/RDFCore/TR/WD-rdf-mt-20030117/#gddenot
then:
(4) <I(rdf:type),I(rdfs:Resource)> in IEXT(I(rdfs:domain)) from (2),(3)
also:
(5) If <x,y> is in IEXT(I(rdfs:domain)) and <u,v> is in IEXT(x) then u is
in ICEXT(y)
-- http://www.w3.org/2001/sw/RDFCore/TR/WD-rdf-mt-20030117/#rdfs_interp
then:
(6) <I(ppp),I(rdf:Property)> in IEXT(I(rdf:type)) from (1),(3)
and:
(7) I(ppp) in ICEXT(rdfs:Resource) from (4),(6) in (5)
[x=I(rdf:type), y=I(rdfs:Resource), u=I(ppp), v=I(rdf:Property)]
and given:
(8) x is in ICEXT(y) if and only if <x,y> is in IEXT(I(rdf:type))
-- http://www.w3.org/2001/sw/RDFCore/TR/WD-rdf-mt-20030117/#rdfs_interp
(9) <I(ppp),I(rdfs:Resource)> in IEXT(I(rdf:type)) from (7) in (8)
so finally:
I( ppp rdf:type rdfs:Resource ) is true from (8) in (3)
QED (this time?)
...
Or, more informally, I think that although IP and IR may be disjoint in
RDF-interpretations, where there is no available vocabulary for this to be
visible or otherwise in an RDF expression, the semantic conditions on RDFS
interpretation require that IP be a subset of IR.
#g
---------------------------------
Graham Klyne <GK@NineByNine.net>
Nine by Nine
http://www.ninebynine.net/
Received on Thursday, 31 July 2003 05:43:48 UTC