FORWARD-CHAINING

make a rule to forward chain when a certain trigger arises
Major Section:  RULE-CLASSES

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.

Examples:

(defthm p-and-r-forward           ; When (p a) appears in a formula to be
(implies (and (p x) (r x))       ; simplified, try to establish (p a) and
(q (f x)))              ; (r a) and, if successful, add (q (f a))
:rule-classes :forward-chaining) ; to the known assumptions.

(defthm p-and-r-forward           ; as above with most defaults filled in
(implies (and (p x) (r x))
(q (f x)))
:rule-classes ((:forward-chaining :trigger-terms ((p x))
:corollary (implies (and (p x) (r x))
(q (f x)))
:match-free :all)))

To specify the triggering terms provide a non-empty list of terms as the value of the :trigger-terms field of the rule class object.

General Form:
Any theorem, provided an acceptable triggering term exists.
The structure of this documentation is as follows. First we give a brief overview of forward chaining and contrast it to backchaining (rewriting). Then we lay out the syntactic restrictions on :forward-chaining rules. Then we give more details about the process and point to a tool to assist you in debugging your :forward-chaining rules.

Overview and When to Use Forward Chaining

Forward chaining is performed as part of the simplification process: before the goal is rewritten a context is established. The context tells the theorem prover what may be assumed during rewriting, in particular, to establish hypotheses of rewrite rules. Forward chaining is used to extend the context before rewriting begins. For example, the :forward-chaining rule (implies (p x) (p1 x)) would add (p1 A) to the context, where A is some term, if (p A) is already in the context.

Forward chaining and backchaining are duals. If a rewrite rule requires that (p1 A) be established and (p A) is known, it could be done either by making (implies (p x) (p1 x)) a :forward-chaining rule or a :rewrite rule. Which should you choose?

As a rule of thumb, if a conclusion like (p1 A) is expected to be widely needed, it is better to derive it via forward chaining because then it is available ``for free'' during the rewriting after paying the one-time cost of forward chaining. Alternatively, if (p1 A) is a rather special hypothesis of key importance to only a few rewrite rules, it is best to derive it only when needed. Thus forward chaining is pro-active and backward chaining (rewriting) is reactive.

Syntactic Restrictions

Forward chaining rules are generated from the corollary term (see rule-classes) as follows. First, every let expression is expanded away (hence, so is every let* and lambda expression), as is every call of a so-called ``guard holder,'' mv-list or return-last (the latter resulting from macroexpansion of calls of prog2\$, must-be-equal or mbe), ec-call, and a few others), or `the'. If the resulting term has the form (implies hyp concl), then concl is treated as a conjunction, with one forward chaining rule with hypothesis hyp created for each conjunct. In the other case, where the corollary term is not an implies, we process it as we process the conclusion in the first case.

Note that unlike rewrite rules, a nested implication is not folded into a single implication. Consider for example the following term.

(implies (p1 x)
(implies (p2 x)
(p3 x)))
Although this term is parsed for a rewrite rule as (implies (and (p1 x) (p2 x)) (p3 x)), that is not the case when this term is parsed for a forward-chaining rule, in which case (p1 x) is treated as the hypothesis and (implies (p2 x) (p3 x)) is treated as the conclusion.

The :trigger-terms field of a :forward-chaining rule class object should be a non-empty list of terms, if provided, and should have certain properties described below. If the :trigger-terms field is not provided, it defaults to the singleton list containing the ``atom'' of the first hypothesis of the formula. (The atom of (not x) is x; the atom of any other term is the term itself.) If there are no hypotheses and no :trigger-terms were provided, an error is caused.

A triggering term is acceptable if it is not a variable, a quoted constant, a lambda application, a let- (or let*-) expression, or a not-expression, and every variable symbol in the conclusion of the theorem either occurs in the hypotheses or occurs in the trigger.