Re: Existentials in backward chaining

I must confess I didn't fully understand Jos' response.

I certainly agree the scope of a query variable is the whole query.  But 
does the scope ever extend beyond the query;  e.g. when combining results 
of several queries (or proof-steps?) to continue the back-chaining 
process?  At this stage, I think I should stop asking questions and start 
reading some more background material.

#g
--

At 03:25 18/06/03 -0700, naudts guido wrote:
>Hallo,
>I agree with Jos. I add that for a query the scope is
>the whole query in my system i.e. this can be more
>than one triple.
>Guido.
>
>--- Jos De_Roo <jos.deroo@agfa.com> wrote:
> >
> > Graham, I'm completely in a hurry but I think it is
> > better to think of bnodes in a premis as of univars
> > with the scope of the rule (taking care of renaming
> > their labels). That follows from the internal ~P V
> > C.
> > This is actually a God's given as a resolution based
> > backward chainer needs such rule scoped univars.
> > For facts, skolem constants take over and it's just
> > for bnodes in conclusions that skolems function
> > terms
> > are needed (function of the rule scoped univars).
> > For a query it's the same story as for a premis.
> >
> >
> > --
> > Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
> >
> >
> >
> >
> >
> >
> >                     Graham Klyne
> >
> >
> >                     <gk@ninebynine       To:     Jos
> > De_Roo/AMDUS/MOR/Agfa-NV/BE/BAYER@AGFA, naudts guido
> >
> >                     .org>
> > <naudts_vannoten@yahoo.com>
> >
> >                                          cc:
> >
> >
> >                     2003-06-17           Subject:
> >  Existentials in backward chaining
> >
> >                     02:49 PM
> >
> >
> >
> >
> >
> >
> >
> >
> >
> >
> >
> >
> > Jos,
> > Guido,
> >
> > I'm thinking about implementing a backward chaining
> > component for my
> > Haskell RDF toolkit, and have noticed a potential
> > problem with existentials
> >
> > (bnodes).  I'm intrigued how you avoid this problem.
> >
> > Here's my test case:
> >
> > Suppose we have a simple rule:
> >
> >       ?f ex:son ?s1 .
> >       ?f ex:son ?s2 .
> >     =>
> >       ?s1 ex:brother ?s2 .
> >
> > To backward chain this requires introducing an
> > existential:  to show
> >     ex:s1 ex:brother ex:s2 .
> > one has to show:
> >     _:f ex:son ex:s1 .
> >     _:f ex:son ex:s2 .
> > for some _:f.
> >
> > Then:
> >     _:s1 ex:sister  ex:d1 .
> >     _:s1 ex:brother ex:s2 .
> > if
> >     _:f ex:son _:s1 .
> >     _:f ex:son ex:s2 .
> > and
> >     _:s1 ex:sister  _:d .
> >
> > but if the original goal is:
> >     _:s1 ex:sister  _:f .
> >     _:s1 ex:brother ex:s2 .
> > one might decide this is true if:
> >     _:f ex:son _:s1 .
> >     _:f ex:son ex:s2 .
> > and
> >     _:s1 ex:sister _:f .
> > which is problematic because if we do a simple union
> > of the graphs we get:
> >     _:f ex:son _:s1 .
> >     _:f ex:son ex:s2 .
> >     _:s1 ex:sister _:f .
> > or if we do a full merge (with bnode renaming):
> >     _:f1 ex:son _:s11 .
> >     _:f1 ex:son ex:s2 .
> >     _:s12 ex:sister  _:f2 .
> > neither of which are the answer we seek.  What we
> > really want to capture
> > is:
> >     _:f1 ex:son _:s1 .
> >     _:f1 ex:son ex:s2 .
> >     _:s1 ex:sister _:f .
> >
> > The problem arises when the bnode introduced by
> > backward chaining clashes
> > with a bnode in some other part of the graph with
> > which the antecedent will
> >
> > subsequently be combined.
> >
> > I have a plan to tackle this, but it feels a bit
> > complicated and wondered
> > if you have an easy strategy top avoid the problem.
> >
> > #g
> >
> >
> > -------------------
> > Graham Klyne
> > <GK@NineByNine.org>
> > PGP: 0FAA 69FF C083 000B A2E9  A131 01B9 1C7A DBCA
> > CB5E
> >
> >
> >
> >
> >
>
>
>__________________________________
>Do you Yahoo!?
>SBC Yahoo! DSL - Now only $29.95 per month!
>http://sbc.yahoo.com

-------------------
Graham Klyne
<GK@NineByNine.org>
PGP: 0FAA 69FF C083 000B A2E9  A131 01B9 1C7A DBCA CB5E

Received on Thursday, 19 June 2003 03:34:45 UTC