Set-fc-criteria
To set the tracking criteria for 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.
Think of the forward chaining criteria as a list of triples, 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.
