Hmmm! This is pretty interesting. It looks as though a lot of this
could be supported by automatic transformations; i.e., a lot of the
typical goal-seeking rule is "boilerplate," so for instance, this rule
as written below
(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))
)
could conceivably be generated from the much simpler
(defrule backch-A-1
;
; one way to realize goal A
;
(need A ?x ?y ?z)
=>
(assert (need D ?y))
(assert (need E ?x ?y ?z))
)
The other stuff might be inferred and automatically inserted; maybe we
need a (declare) statement to give some hints, or maybe a
(set-backchain-reactive A) command might be enough.
Thanks for working this out! This will be filed in my "interesting
things to work on" pile.
I think [EMAIL PROTECTED] wrote:
> 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]
> ---------------------------------------------------------------------
>
---------------------------------------------------------
Ernest Friedman-Hill
Distributed Systems Research Phone: (925) 294-2154
Sandia National Labs FAX: (925) 294-2234
Org. 8920, MS 9012 [EMAIL PROTECTED]
PO Box 969 http://herzberg.ca.sandia.gov
Livermore, CA 94550
---------------------------------------------------------------------
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]
---------------------------------------------------------------------
