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
      Skolemization
    - 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
      Skolemization
    - So maybe we should go ahead and just put it in BLD (and perhaps 
      Core). 

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
that?

    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
        consequent. 

Yes?

     -- Sandro

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