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:
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:
(which is something you do not want to derive)

Best, Jos

>     -- Sandro


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

Received on Friday, 23 May 2008 14:42:12 UTC