Re: production rule object creation actions and frame axioms

On Wed, 13 Aug 2008 12:02:22 -0700
Gary Hallmark <gary.hallmark@oracle.com> wrote:

> 
> 
> 
> Michael Kifer wrote:
> > On Tue, 12 Aug 2008 15:52:13 -0700
> > Gary Hallmark <gary.hallmark@oracle.com> wrote:
> >
> >   
> >> By "skolem function" I meant "logical function used to remove 
> >> existential quantification", e.g.
> >>
> >>     forall ?X exists ?Y parent(?X,?Y) :- person(?X).
> >>
> >> =>
> >>
> >>     forall ?X parent(?X, f01(?X)) :- person(?X).
> >>
> >> where f01 is unique in the ruleset.
> >>
> >> I think that at least logical functions that are used to skolemize should be
> >> allowed in Core.
> >>     
> >
> > How do you distinguish skolem functions from other functions?
> > It is just a unique function symbol -- nothing more. 
>
> It's a bit more.  It also includes all the in-scope universally 
> quantified variables as arguments.

Any function symbol can be viewed this way.

 
> It's easy to distinguish the skolem functions - they are the ones that 
> can be de-skolemized.  I.e.
> all occurrences are in the head of one rule or in the body of one rule. 

You can perform the same procedure in many cases for any function symbol.
If quantification prefix weren't linear then you could have done this in all
cases.

> > (By adding them to BLD I
> > meant adding syntax and semantics for simplifying their use. Conceptually there
> > is not much of a diff.)
> >
> > What I was trying to say (but forgot to add one rule) is that you can create
> > nonterminating processes whether the func symbol is unique or not:
> >
> > forall ?X parent(?X, f01(?X)) :- person(?X).
> > forall ?X ?Y person(?Y) :-  parent(?X, ?Y).
> >
> > so here you go ad infinitum.
>
>
> Yeah, but its no worse than, e.g. func:concat or func:numeric-add.  
> Unless you also want to remove most of the builtins, you can't get rid 
> of infinity, and skolem functions seem tractable for a PRD translator to 
> implement, that's why I think they should be in Core.


For builtins you can come up with more or less reasonable restrictions.
For skolems you most likely cannot. With existentials the logic becomes
undecidable and it is not clear what to do here.

The more important point is that you cannot really distinguish skolems from
non-skolems, as I pointed out above.

michael
and

Received on Wednesday, 13 August 2008 19:39:04 UTC