Re: Existentials in backward chaining

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

Received on Tuesday, 17 June 2003 16:26:12 UTC