Re: production rule object creation actions and frame axioms

Can you give an example of a ruleset with a logical function that occurs 
only the head or the body (not both) of a single rule but is not a 
skolem function (i.e. cannot be replaced with an existentially 
quantified variable)?

I was hoping to "support" skolem functions (but no other logical 
functions) in PRD by translating skolems in the head (only those that 
occur in the "object" position of a classification) to a call to the 
class constructor, and translating skolems in the body to an 
existentially quantified variable.

Michael Kifer wrote:
>
> 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 20:49:28 UTC