Major Section: FORWARD-CHAINING-REPORTS

Examples: (set-fc-criteria) ; shut off all tracking (set-fc-criteria nil) (set-fc-criteria t) ; to track all forward chaining (set-fc-criteria (t t t)) (set-fc-criteria ((:FORWARD-CHAINING LEMMA1) ; track all uses of LEMMA1, t t) ((:FORWARD-CHAINING LEMMA2) ; uses of LEMMA2 triggered (ALISTP (BASIC-MAPPER A B)) ; by this specific ALISTP term t) (t t (TRUE-LISTP (DLT D)))) ; and every rule deriving ; this TRUE-LISTP term. General Forms: (set-fc-criteria nil) (set-fc-criteria t) (set-fc-criteria triple1 triple2 ...)where each triple is of the form

`(rune inst-trigger inst-concl)`

. If rune
is non-`t`

is must be a forward chaining rune. The other two
components, `inst-trigger`

and `inst-concl`

, if non-`t`

, must be terms.
The list of all the triples supplied is called the ``criteria.'' In the form
`(set-fc-criteria nil)`

, the criteria used is the empty list of triples.
(Technically, supplying `nil`

as a triple ``ought'' to be an error, but it
is a more ``natural'' way to say the list of criteria is empty than to use
the correct form `(set-fc-criteria)`

.) In the form `(set-fc-criteria t)`

the criteria used is the list containing the single triple `(t t t)`

.This function sets the tracking criteria for forward chaining reporting. See forward-chaining-reports for a general discussion of tracking and reporting forward chaining activity.

The forward chaining criteria is a list of triples. Think of it as
representing a disjunction of conjunctions. The activation of a
`:`

`forward-chaining`

rune by some triggering term in the current
context *satisfies* the criteria if it satisfies one of the triples. To
satisfy the triple `(rune inst-trigger inst-concl)`

, the activation must
satisfy each component of the triple. Any `t`

component is always
satisfied. If `rune`

is non-`t`

it is satisfied if the activation is
for the given rune. If `inst-trigger`

is non-`t`

, it is satisfied if
the activation is triggered by the given term.
(```Inst-trigger''`

stands for ``instantiated trigger.'' It is not the
trigger term of the rule but is supposed to be an instance of that term that
you believe will arise in some proof attempt you are debugging -- an instance
you want to ``watch'' as it fires the rule.) If `inst-concl`

is non-`t`

,
it is satisfied if the activation could possibly derive the conclusion
given. (Again, ```inst-concl''`

stands for ``instantiated conclusion'' and
shows the term in your problem that you expect to be derived by forward
chaining.)

Note that if the criteria is empty, it is never satisfied, so
tracking is turned off. If the criteria is the singleton
list containing just the triple `(t t t)`

, then every
activation satisfies it and so all `:forward chaining`

rules are tracked.

See forward-chaining-reports for details.