Re: production rule object creation actions and frame axioms

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.

I  understand that BLD cannot retract but PRD can.  That's fine, we have 
PRD-specific syntax and semantics for that.  I'm just concerned about 
using a BLD ruleset with my Javabeans as data.  A Javabean is a 
constrained frame, and we need a way to express those constraints -- as 
rules, as some syntactic sugar, or as owl statements.  Or maybe we can 
find a use for external frames here?

Michael Kifer wrote:
> Gary,
> Thanks for the helpful analysis. Some comments within.
>
>
> On Tue, 12 Aug 2008 12:26:29 -0700
> Gary Hallmark <gary.hallmark@oracle.com> wrote:
>
>   
>> One could use existential quantification in the conclusion to express 
>> object creation:
>>
>> exists ?e And(?e#Employee ?e[empNo->?ssn salary->50000]) :- 
>> And(?p#Person ?p[ssn->?ssn college->"MIT"])
>>
>> Because we would like to share the same solution with BLD, we skolemize 
>> (using "f") the above to
>>
>> And(?e#Employee ?e[empNo->?ssn salary->50000]) :- And(?p#Person 
>> ?p[ssn->?ssn college->"MIT"] ?e=f(?p ?ssn))
>>
>> We can limit PRD's use of logical functions to skolem functions.
>>     
>
> BLD does not have skolem functions. I remember we discussed this, but in the
> end you said that you do not need them, so I did not add them to avoid delaying
> the last call (and possibly facing objections from others, which would have
> delayed even further). Now that we are in the last call, I do not know whether
> adding such a substantial thing as a skolem can be done.
>
> Furthermore, even with Skolem functions you can create non-terminating
> bottom-up derivations. For instance,
>
>     forall ?X exists ?Y parent(?X,?Y) :- person(?X).
>
> At today's telecon I heard that decidability for the core is a must, and Jos
> even said he does not see any use for function symbols.
>
> I could not add my 0.02c because I lost the Inet connection and could not
> unmute my phone :-(
>
>   
>> To support removing an object, we need to be able to retract its 
>> classification as well as remove its slots:
>>
>> Forall ?e ?sn ?sv (Do(Retract(?e#Employeee) Retract(?e[?sn->?sv]) ) :- 
>> ?e#Employee
>>
>> Because the semantics of frames differs from the more typical Javabeans, 
>> as mentioned above, we need to account for this difference.  E.g. 
>> consider the following rule set:
>>
>> Joe#Employee
>> Joe[salary->40000]
>> ?e[salary->?salary * 1.1] :- And(?e#Employee ?e[salary->?salary] ?salary 
>> < 48000)
>>
>> With frame semantics, a model is Joe[salary->40000 salary->44000 
>> salary->48400].  With Javabean/PRD semantics, we must have a final 
>> configuration with only Joe[salary->48400] (or maybe Joe[salary->44000] ??)
>>     
>
>
> It is not that the semantics of frames is different. Here we have logical
> rules, and this is their semantics. Using this first-order semantics you cannot
> retract old knowledge. This is outside not only of the core, but also BLD.
>
>
> 	--michael  
>

Received on Tuesday, 12 August 2008 22:58:58 UTC