SET-FC-CRITERIA

to set the tracking criteria for forward chaining reports 
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.