# Re: adding existentials and conjunctions to BLD consequents

From: Jos de Bruijn <debruijn@inf.unibz.it>
Date: Fri, 23 May 2008 16:41:27 +0200
Message-ID: <4836D797.3030305@inf.unibz.it>
To: Sandro Hawke <sandro@w3.org>

```

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

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

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:47:50 UTC