To see reports about the forward chaining process

Debugging forward-chaining rules can be hard because their effects are not directly visible on the goal. In this documentation we tell you how to get reports on the forward chaining activity occurring in your proof attempts. This documentation is written in several parts. The first part is an introduction for the first-time user of forward chaining reports. The next two parts describe how to read reports. The last part describes how to monitor forward chaining activity only for selected runes, etc. We recommend the new user of these reports read everything!

*A Quick Introduction to Forward Chaining Reports*

Caution: The reporting mechanism maintains some state, and if you have already used forward chaining reporting in a session, the directions below may not work as advertised! To return to the default forward chaining reporting state, execute this form at the top level:

(reset-fc-reporting)

You can get a report about all forward chaining activity in subsequent proofs by doing:

(set-fc-criteria t)

Options will be discussed later that allow you to monitor the activity
caused by particular

Then do a proof that is expected to cause some forward chaining. In the proof output you will see lines like this:

(Forward Chaining on behalf of PREPROCESS-CLAUSE: (FC-Report 1))

This is the only difference you should see in the proof output.

After the proof attempt has terminated, you can execute:

(fc-report k)

for any

If you want to see these reports in real time (embedded in the proof output), do this before invoking the prover:

(set-fc-report-on-the-fly t)

Collecting the data used to generate these reports slows down the prover. If you no longer wish to see such reports, do

(set-fc-criteria nil)

*How To Read FC Reports*

The report printed by

Forward Chaining Reportk: Caller:tokenClause: (lit1lit2...litn) Number of Rounds:mContradictionp:boolActivations: (act1act2...)

This report means that the *k*th use of forward chaining in the most
recent proof attempt was done on behalf of *token* (see below). The
initial context (set of assumptions) consisted of the negations of the
literals listed in the clause shown and the initial candidate trigger terms
are all those appearing in that clause. This invocation of forward chaining
proceeded to do *m* rounds of successive extensions of the initial
context and ultimately either reached a contradiction (*bool* = *bool* =

Forward chaining is done on behalf of many proof techniques in the system.
Each is associated with a *token*. The main proof technique that uses
forward chaining is `induction`
rules, and the definitional principle (and related utilities such as `verify-termination` and `verify-guards`) which uses forward chaining
during the construction of both measure conjectures and guard conjectures.
When used this way, the *token* is

*How to Read Activation Reports*

The forward chaining report concludes with a list of activation reports.

Activations: (act1act2...)

Each *acti* is of the form:

(rune(:TRIGGERinst-trig) ((:UNIFY-SUBSTsubst) (:DISPOSITIONoutcome-part1outcome-part2inst-term)) ...)

where the *disposition* of the activation and each disposition
describes a substitution *subst* identifying the final instantiation of
the rule and how the activation fared. Suppose there are *n*
dispositions. (If the rule in question contains no free variables, *n*
will be 1.)

This activation report means that during the forward chaining process in
question, the `forward-chaining` rune *rune* was fired
due to the presence in the evolving context of the trigger term
*inst-trig*. (Note that *inst-trig* is an instantiation of the
trigger term of the named rule. That is, the variable symbols you see in
*inst-trig* are those of the clause printed in the forward chaining
report.) The activation of *rune* by *inst-trig* proceeded to split
*n* ways as different choices were made for the free-variables
occurring among the hypotheses. Each of those *n* choices gave rise to a
different substitution *subst*, and each succeeded or failed as described
by the corresponding

The *outcome-part1*, *outcome-part2*, and *inst-term*.
*Outcome-part1* is either *subst* either succeeded in the sense that all of its
instantiated hypotheses were found in the context, or failed because some
instantiated hypothesis was not found.

If *inst-term* is the
instantiated conclusion produced by the rule. *Outcome-part2* is
*Outcome-part2* is *Outcome-part2* is

If *inst-term* is an
instantiated hypothesis of the rule that is assumed false in the current
context, *inst-term* is an
instantiated hypothesis whose truth value is not determined by the context, or
*inst-term* is an oddly
instantiated hypothesis whose truth value is not determined by the context and
which also contains free variables. In the last case, the ``odd''
instantiation was by the substitution *subst* but extended so that free
variables in the hypothesis are renamed to start with the prefix

Note: All of the terms printed in the report are instantiated with the relevant unifying substitution (possibly extended to bind free variables).

*Specifying the Tracking Criteria*

During a proof attempt, the forward chaining module stores information
about the activations satisfying certain criteria. The *criteria* is a
list of triples. Each triple consists of a forward chaining rune, an
instantiated trigger term, and an instantiated conclusion to watch for.
However, any or all of the components of such a triple may be

An activation *could* produce the
instantiated conclusion (with the right choice of any free variables).

Thus, the criteria is interpreted as a disjunction of conjunctions, making it possible to track a specific set of runes, triggers, and conclusions.

For example, here is a triple that might appear in the criteria:

((:FORWARD-CHAINING ALISTP-FORWARD-TO-TRUE-LISTP) t t).

This triple would cause every activation of the given rule to be tracked. However, the triple

((:FORWARD-CHAINING ALISTP-FORWARD-TO-TRUE-LISTP) (ALISTP (MAKE-BINDINGS VARS (TOP-N (OP1 INST) (STACK S)))) t)

would only track activations of that rule fired by the specific term shown as the second element of the triple. Furthermore

(t (ALISTP (MAKE-BINDINGS VARS (TOP-N (OP1 INST) (STACK S)))) t)

would track any forward chaining rule triggered by that term, and

(t t (TRUE-LISTP (MAKE-BINDINGS VARS (TOP-N (OP1 INST) (STACK S)))))

would track any rule fired by any trigger that might lead to the specific term given as the third component above.

Note: The condition on how an activation satisfies an instantiated conclusion is a little subtle. Consider the activation of the forward chaining rule

(implies (and (symbol-listp x) (equal (len x) (len y))) (true-listp (make-bindings x y)))

triggered by *could* produce the specific conclusion shown in the last
triple above, if it just happened that

Observe that the triple

(t t t)

is satisfied by every activation of any rule by any trigger term producing any conclusion.

The function

(set-fc-criteria ((:FORWARD-CHAINING LEMMA1) t t) ((:FORWARD-CHAINING LEMMA2) (ALISTP (BASIC-MAPPER A B)) t) (t t (TRUE-LISTP (DLT D)))),

the system would track all activations of the forward-chaining rule

Because criteria generally mention variable symbols used in a specific conjecture, it is probably best to reconsider your criteria every time you want to track forward chaining.

If the criteria is

To track every forward chaining activation you may set the criteria with
either

If, when you read a forward chaining report, you see no mention of an
activation you have in mind, e.g., of a certain rune or deriving a certain
conclusion, and you have set the criteria correctly, then the activation never
happened. (This is akin to using `brr` and `monitor`
to monitor the application of a rewrite rule and then seeing no interactive
break.)

For some relevant functions to help you manage criteria and when the full
reports are printed see `fc-report`, `show-fc-criteria`, `set-fc-criteria`, `reset-fc-reporting`, and `set-fc-report-on-the-fly`.

- Set-fc-criteria
- To set the tracking criteria for forward chaining reports
- Set-fc-report-on-the-fly
- To determine when forward-chaining reports are printed
- Reset-fc-reporting
- Reset the forward-chaining tracking state to its initial configuration
- Fc-report
- To report on the forward chaining activity in the most recent proof
- Show-fc-criteria
- Print the forward-chaining tracking criteria