Re: adding existentials and conjunctions to BLD consequents

Sandro Hawke wrote:
>> I'm afraid that adding existentials to rule heads pushes the language 
>> outside of Horn.  In fact, we would nearly have full first-order logic 
> 
> How so?   You can just get rid of it by Skolemizing it.
> 
> This is a typical N3 Rule, saying that for every two things with a
> grandparent relation, there exists a third thing connected to those
> things by a parent relation:
> 
>    { ?x :grandparent ?y. }
>    =>
>    # read "[ ... ]" as "something which has ..."
>    { ?x :parent [ :parent ?y ] }.
> 
> I would turn that into this BLD:
> 
>    ?x[parent->sk1(?x,?y)] :- ?x[grandparent->?y]
> 
>    sk1(?x,?y)[parent->?z] :- ?x[grandparent->?y]
> 
> The results to all positive ground queries on these two rule bases would
> be the same, wouldn't they?

One can reduce reasoning with existentials to reasoning with Skolem 
functions, but from a representation point of view the things are quite 
different.  Specifically, when using a function symbol, you make a much 
stronger statement, because you name the function.

For example, from your above rules and the fact:
a[grandparent->b]
we can derive the following:
Exists ?x a[parent->?x] and ?x[parent->b]
(which is what you want to derive in this case)

But also:
a[parent->sk1(a,b)]
(which is something you do not want to derive)


Best, Jos

> 
>     -- Sandro
> 

-- 
                          debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
One man that has a mind and knows it can
always beat ten men who haven't and don't.
   -- George Bernard Shaw