I've just come back from vacation to find that my past two attempts
to send this (first to Ernest only, then to the list) have failed.
So I'm trying again. Perhaps the internet gremlins are so offended
by what I've done here that they don't want to transmit it.

It's a bit of jess code that illustrates how backtracking can be
implemented to support a richer form of backchaining.

What I've done here is independent of Jess's current backchaining,
although it follows the basic idea. It is an implementation for a
specific case, which I devised to cause a couple of backtracks. 
But the pattern of rules should make it clear how it would be 
generalized.

There are three key points:

1. Each backward chaining rule - i.e., each Horn clause that you want to

do backward chaining over - actually needs two Jess rules: one to
decompose the goal into subgoals (NeedA -> Need B & NeedC), and one 
to establish (compose) the goal once the subgoals have been established 
(B & C -> A). My theorem-proving colleague Dave Barker-Plummer pointed 
out that this corresponds in theorem-proving terms to a) tactics, and 
b) inference rules.

2. There are two fact types, (trying-for ...) and (failed-attempt ...)
that keep track of the rule and variable binding used  in any particular
step through the (implicit) search tree. These are negated as CEs in the
decomposition rules to prevent re-trying something that was already tried, 
as well as to enable other decomposition rules that haven't yet
failed.

The ubiquitous ?tag variable is there in order to keep separate any unrelated 
backchaining operations that might happen to have some subgoals in common.

Curiously, if I understand what I have done here, the backtracking over
choice of rule is effected by the decomposition rules, while backtracking over
variable bindings is implicitly effected by the composition rules
(taking advantage of the Rete algorithm).

3. The saliences of the cleanup rules and the particular guard (negated)
CEs were a bear to arrive at, and the whole thing will break if they are
so much as breathed on. I've noted some of the rationale in comments, but
probably not enough.

If you run the file (there's a run command at the bottom of the file),
you'll see the backtracking occurring. I don't have a mathematical proof that it is
correct in the general case, but I tentatively believe it is.

Cheers,
Sidney C. Bailin
Knowledge Evolution, Inc.

;;;;;;;;;;;;;;;;;;;;;;;;;

(clear)
(watch all)
;(unwatch facts)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rules for realizing goal A ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defrule backch-A-1
        ;
        ; one way to realize goal A
        ;
        ?n <- (need A ?tag ?x ?y ?z)
        (not (failed-attempt A 1 ?tag ?x ?y ?z))
        (not (trying-for A ? ?tag ?x ?y ?z))
=>
        ;(retract ?n)
        (assert (trying-for A 1 ?tag ?x ?y ?z))
        (assert (need D ?tag ?y))
        (assert (need E ?tag ?x ?y ?z))
)

(defrule backch-A-2
        ;
        ; another way to realize goal A
        ;
        ?n <- (need A ?tag ?x ?y ?z)
        (not (failed-attempt A 2 ?tag ?x ?y ?z))
        (not (trying-for A ? ?tag ?x ?y ?z))
=>
        ;(retract ?n)
        (assert (trying-for A 2 ?tag ?x ?y ?z))
        (assert (need B ?tag ?x ?y))
        (assert (need C ?tag ?y ?z))
)

(defrule fwdch-A-1
        (B ?tag ?u ?v)
        (C ?tag ?v ?w)
        ;
        ;either any val will do, or it must match the other conditions
        ;
        ?t <- (trying-for A ?rule ?tag ?x&nil|?u ?y&nil|?v ?z&nil|?w) 
        (not (failed-attempt A ?rule ?tag ?u ?v ?w))
=>
        (retract ?t)
        (assert (A ?u ?v ?w))
)

(defrule fwdch-A-2
        (D ?v)
        (E ?u ?v ?w)
        ?t <- (trying-for A ?rule ?tag ?x&nil|?u ?y&nil|?v ?z&nil|?w) 
        (not (failed-attempt A ?rule ?tag ?u ?v ?w))
=>
        (retract ?t)
        (assert (A ?u ?v ?w))
)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rules to cleanup an attempt ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defrule failed-attempt
        (declare (salience -995))
        ?t <- (trying-for ?goal ?rule ?tag $?x)
=>
        (retract ?t)
        (assert (failed-attempt ?goal ?rule ?tag $?x))
        ;(assert (need ?goal ?tag $?x)) ;backtrack
)
(defrule failed-after-trying
        (declare (salience -996))
        ?n <- (need ?goal ?tag $?x)
        ?f <- (failed-attempt ?goal ?rule ?tag $?x)
=>
        (retract ?n)
        (retract ?f)
)
(defrule failed-without-even-trying
        (declare (salience -997))
        ?n <- (need ?goal ?tag $?x)
=>
        (retract ?n) ; give up
)
(defrule also-failed-after-trying-this ;residuals
        (declare (salience -998))
        ?f <- (failed-attempt ?goal ?rule ?tag $?x)
=>
        (retract ?f)
)
(defrule succeeded-so-dont-need-anymore
        (declare (salience 999)) ;do right away to prevent restarting the process
        ?n <- (need A ?tag ?x ?y ?z)
        (A ?x ?y ?z)
=>
        (retract ?n) 
)

        
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rules for realizing goal B ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defrule backch-B-1
        ;
        ; one binding that realizes goal B
        ;
        ?n <- (need B ?tag ?x&cat|nil ?y&dog|nil)
=>
        (retract ?n)
        (assert (B cat dog))
)
(defrule backch-B-2
        ;
        ; another binding that realizes goal B
        ;
        ?n <- (need B ?tag ?x&bird|nil ?y&mouse|nil)
=>
        (retract ?n)
        (assert (B bird mouse))
)
(defrule backch-B-2
        ;
        ; another binding that realizes goal B
        ;
        ?n <- (need B ?tag ?x ?y)
        (test (< (str-length (str-cat ?x ?y)) 328))
=>
        (retract ?n)
        (assert (B ?x ?y))
)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rules for realizing goal C ;
; (similar to A)             ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defrule backch-C-1
        ;
        ; another way to realize goal C
        ;
        ?n <- (need C ?tag ?y ?z)
        (not (failed-attempt C 1 ?tag ?y ?z))
        (not (trying-for C ? ?tag ?y ?z))
=>
        ;(retract ?n)
        (assert (trying-for C 1 ?tag ?y ?z))
        (assert (need J ?tag ?y))
        (assert (need K ?tag ?y ?z))
)
(defrule backch-C-2
        ;
        ; one way to realize goal C
        ;
        ?n <- (need C ?tag ?y ?z)
        (not (failed-attempt C 2 ?tag ?y ?z))
        (not (trying-for C ? ?tag ?y ?z))
=>
        ;(retract ?n)
        (assert (trying-for C 2 ?tag ?y ?z))
        (assert (need H ?tag ?y ?z))
        (assert (need I ?tag ?z))
)


(defrule fwdch-C-1
        ;
        ;either any val will do, or it must match the other conditions
        ;
        (H ?tag ?v ?w)
        (I ?tag ?w)
        ?t <- (trying-for ? ?rule ?tag ?y&nil|?v ?z&nil|?w) 
        (not (failed-attempt C ?rule ?tag ?v ?w))
=>
        (retract ?t)
        (assert (C ?v ?w))
)

(defrule fwdch-C-2
        (J ?tag ?v)
        (K ?tag ?v ?w)
        ?t <- (trying-for C ?rule ?tag ?y&nil|v ?z&nil|?w) 
        (not (failed-attempt C ?rule ?tag ?v ?w))
=>
        (retract ?t)
        (assert (C ?v ?w))
)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rules for realizing goal D ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defrule backch-D
        ?n <- (need D ?tag ?x)
=>
        (retract ?n)
        (assert (D ?x))
)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rules for realizing goal E ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defrule backch-E
        ?n <- (need E ?tag ?x ?y ?z)
=>
        (retract ?n)
        (assert (E ?x ?y ?z))
)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rules for realizing goal H ;
; (similar to B)             ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defrule backch-H-1
        ;
        ; one binding that realizes goal H
        ;
        ?n <- (need H ?tag ?x&kitten|nil ?y&rat|nil)
=>
        (retract ?n)
        (assert (H kitten rat))
)
(defrule backch-H-2
        ;
        ; another binding that realizes goal H
        ;
        ?n <- (need H ?tag ?x&puppy|nil ?y&aardvark|nil)
=>
        (retract ?n)
        (assert (H puppy aardvark))
)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rules for realizing goal I ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defrule backch-I
        ?n <- (need I ?tag ?x&cat|dog|puppy|bird|mouse|rat|aardvak)
=>
        (retract ?n)
        (assert (I ?x))
)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(assert (need A 111 cat dog nil))

(run)


--------------60C956FF483FAA4AF4481428--




----- End Included Message -----

---------------------------------------------------------------------
To unsubscribe, send the words 'unsubscribe jess-users [EMAIL PROTECTED]'
in the BODY of a message to [EMAIL PROTECTED], NOT to the
list (use your own address!) List problems? Notify [EMAIL PROTECTED]
---------------------------------------------------------------------

Reply via email to