Re: Fitting PR and RR into logical rules

> > Specifically, here's my strawman.   I propose the ECA/Reaction rule:
> > 
> >     on Event
> >     when Condition
> >     then Action
> > 
> > be treated semantically as the Horn rule (FOL implication):
> > 
> >     if eventHappened(Event) and Condition
> >     then actionRequested(Action)
> > 
> > and similarly for production rules (just drop the event part).
> 
> I'm not sure that this would result in *any* inferences in a FOL system.
> How are you going to put the eventHappened and actionRequested into the FOL
> (or other deductive) framework in such a way that supports, for example,
> chaining of rules?

I'll refine the sketch a little:

 1. When an event occurs, facts are added to the rulebase
    to describe the occurance.  To use RIF-UCR 1.1 and
    make the delivery of a perishable item an event, the
    facts that get added to the rule base might be:

       eventHappened(ev331).
       deliveryEvent(ev331, item7, date(2006,06,02)).

    where "ev331" is some new identifier made up by the component that
    adds things to the rule base.  The rulebase would probably already
    contain stuff about item7, like:

       perishable(item7).
       scheduledDelivery(item7, date(2006,05,02)).

 2. The rule 

         "If an item is perishable and it is delivered more than 10 days
         after the scheduled delivery date then the item will be
         rejected."

    might be written in FOL (+date math) like this, keeping the ECA
    spirit of that rule:

        all Event Item DateDelivered DateDeliveryScheduled (
             ( eventHappened(Event) &
               deliveryEvent(Event, Item, DateDelivered) &
               perishable(Item) &
               scheduledDelivery(Item, DateDeliveryScheduled) &
               late(DateDelivered, DateDeliveryScheduled)
             ) -> (
               exists Action (
                 actionRequested(Action, deliveryRejection(Item))
             ))
        ).

 3. For the action to be performed in this sketch, some component
    outside the reasoner will need to query for actionRequested things. 
    So we query for 

        actionRequested(ActionID, Details))

    which in a resolution theorem prover is done by asserting the
    negation and looking for a contradiction; ie asserting:

        -(exists ActionID Details actionRequested(ActionID, Details)).

    and then looking in the proof to see how Action was instantiated in
    that proof step.  Really, you'll have to look for all the proofs and
    keep track of which Actions you've already performed.  In a normal
    resolution theorem prover, Action will be Skolemized into a function
    term like sk1(Event, Item, DateDelivered, DateDelieveryScheduled) --
    something which will work as a unique identifier to prevent the same
    action from running twice.

I did happen to run this through the classic FOL theorem prover Otter
(using a manual assertion: late(date(2006,06,02), date(2006,05,02)) for
now) and the proof included the deduction:
   
actionRequested($f1(ev331,item7,date(2006,06,02),date(2006,05,02)),
                deliveryRejection(item7)).

Again, I'm not saying I'd expect Otter or any other FOL theorem prover
to be an effective ECA engine, I'm using it to be clear about this
approach to mostly-unified semantics.

I'll be interested to hear how these semantics differ from those
implemented in RR/PR systems, and which semantics business rule
developers would prefer.

    -- Sandro

Received on Friday, 2 June 2006 19:28:32 UTC