Forall quantifier facts order

[vranoch]

Hello Gary,

could You please explain me, why the following 2 rules behave differently (A fires and B does not) on the same facts? They differ just in the order of one fact.

Thanks Vranoch

(deffacts XY
    (LVAR LV-arr 1 "A")
    (LVAR LV-arr 1)
    (LVAR LV-arr 2 "B")
    (LVAR LV-arr 2)
    (LVAR LV-arr 3 "A")
    (LVAR LV-arr 3)
    (LVAR LV-arr 4 "A")
    (LVAR LV-arr 4)

    (IX X1 1)
)

(defrule A ""
    (forall 
;       (LVAR LV-arr ?IX_1 )
        (IX X1 ?X1)
        (LVAR LV-arr ?IX_1 )
        (LVAR LV-arr ?X1 ?X1_var)
        (LVAR LV-arr ?IX_1 ?IX_1_var)
        (test (eq  ?X1_var ?IX_1_var))
    )

=>
    (printout t "FIRED - NEW" crlf)
)

(defrule B ""
    (forall 
        (LVAR LV-arr ?IX_1 )
        (IX X1 ?X1)
;       (LVAR LV-arr ?IX_1 )
        (LVAR LV-arr ?X1 ?X1_var)
        (LVAR LV-arr ?IX_1 ?IX_1_var)
        (test (eq  ?X1_var ?IX_1_var))
    )

=>
    (printout t "FIRED - ORIG" crlf)
)

[Gary Riley]

The forall conditional element is translated from

(forall <CE-1>
        <CE-2>
           .
           .
           .
        <CE-N>)      

to

(not (and <CE-1>
          (not (and <CE-2>
                       .
                       .
                       .
                    <CE-N>))))

The first conditional element can't be exchanged with one of the other conditional elements without changing the logic. Consider the difference between these two statements:

The team is ready if everyone who is playing has practiced.
The team is ready if everyone who has practiced is playing.

[vranoch]

OK, got it. Thanks Vranoch