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>

CC: public-rif-wg@w3.org

Date: Fri, 23 May 2008 16:41:27 +0200

Message-ID: <4836D797.3030305@inf.unibz.it>

To: Sandro Hawke <sandro@w3.org>

CC: public-rif-wg@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 ShawReceived 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
*