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)

I think you've switched arguments here.

My points were:

    - many rule systems have existentials in the consequent (at
      least with gensym semantics)
    - it's straightforward to implement in translation, via
    - so that we can go between systems that have it, via RIF, like 
      N3->RIF->Jena, without badly contorting the rules, we'll need
      an extension for it -- and the fallback transform will do the
    - So maybe we should go ahead and just put it in BLD (and perhaps 

I don't dispute that Skolemizing changes the semantics in some ways.
The question is, at which of these three possible places do we handle

    1.  at the point where I turn N3 into BLD
    2.  after turning N3 into BLD+Extension, at the point where there's a
        fallback translation to remove the Extension
    3.  if it's in BLD, at the point where BLD is being translated to
        some native language which does not support existentials in the


     -- Sandro




Received on Friday, 23 May 2008 15:03:15 UTC