- From: <jos.deroo.jd@belgium.agfa.com>
- Date: Tue, 28 Aug 2001 22:48:36 +0100
- To: phayes@ai.uwf.edu
- Cc: jos.deroo.jd@belgium.agfa.com, w3c-rdfcore-wg@w3.org
Hi Pat,
> > > In danger of making another mistake ....
> > >
> > > I didn't quite see how the interpolation lemma worked when the LHS has
> > > anonymous nodes.
> > >
> > > How does it get the following entailment
> > >
> > >
> > > _:x <b> <c> .
> > >
> > >
> > > entails
> > >
> > > _:y <b> <c> .
> >
> >I just see that we have a bug in our stuff...
> >for
> > _:x <b> <c>. |=> _:y <b> <c>.
> >we assert LHS and query it with RHS
> >and i think we should query with
> > {_:y <b> <c>} log:forAll _:y.
> >and then there is a match found with
> > {_:x <b> <c>} log:forSome _:x.
> >(i have to think about that, and try...)
>
> That seems right to me. The log:forAll on the RHS tells the reasoner
> it is free to substitute anything for the variable, right?
Well I think I was wrong with that forAll
that entailment doesn't seem to make sense
We have it now like
==== jeremy3.nt
_:x <b> <c>.
====
==== jeremy4.nt
_:y <b> <c>.
====
====
C:\n3>java Euler -core -trace jeremy3.nt jeremy4.nt
@@ assert [] <b> <c>.
[1]CALL: [] <b> <c>.
[1]EXIT: [] <b> <c>.
@@ continue
# Generated with http://www.agfa.com/w3c/euler/#27.055 on Tue Aug 28 21:16:35 CEST 2001
# for query file:/n3/jeremy4.nt
# given [file:/n3/jeremy3.nt]
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
[] <b> <c>.
# Proof found for file:/n3/jeremy4.nt in 1 step (573 steps/sec)
====
so like 'blank' node tokens
But if we have
e.g.
{:s [ :subPropertyOf :p] :o} log:implies {:s :p :o}.
we treat it like
{:z :subPropertyOf :p. :s :z :o} log:implies {:s :p :o}.
where :z is universally quantified
and that seems to work quite well
and BTW for so called 'variable' predicates we find
your MT thing/extension distinction really wonderful!
(I mean the :z once in subject and once in predicate
position and treating them without and with extension)
--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Tuesday, 28 August 2001 16:48:50 UTC