- From: <jos.deroo.jd@belgium.agfa.com>
- Date: Fri, 21 Dec 2001 23:40:22 +0100
- To: pfps@research.bell-labs.com
- Cc: bwm@hplb.hpl.hp.com, mmoran@netphysic.com, dave.beckett@bristol.ac.uk, www-rdf-interest@w3.org
[...]
> I don't think that your manipulations are permissable, at least not in
> RDF(S).
>
> In particular, entailment is a meta-theoretic notion, and is not part of
> the syntax of a logical formalism. Some logical formalisms can turn some
> or all entailments into implication, but not all can.
classical logic can
> In any case, I'm still confused as to what you were trying to demonstrate.
> Perhaps you were trying to show that RDF(S) is a fragment of first-order
> logic.
We just do and don't do something with RDF graphs
e.g.
given RDF graph1
_:child gc:childIn _:family .
_:parent gc:spouseIn _:family .
and RDF graph2
_:aaa gc:parent _:bbb .
all the rest is about what we do and don't do with these RDF graphs
don't assert graph1
don't assert graph2
state that bnode _:child denotes same thing as bnode _:aaa
state that bnode _:parent denotes same thing as bnode _:bbb
state that graph1 classic-logically implies graph2
one way to write this down is
{ ?child gc:childIn ?family . ?parent gc:spouseIn ?family }
log:implies { ?child gc:parent ?parent } .
where ?child, ?family and ?parent are universally quantified
(although, if there would have been other bnodes in graph2,
they would remain existentially quantified)
now we treat that as another RDF statement
(but again, not necessarily asserted)
so that we can repeat the same story
I don't know what one could claim from this
w.r.t. FOL (or SWOL)
--
Jos
Received on Friday, 21 December 2001 17:42:19 UTC