## MetaPRL Proof Caching and Chaining

You can read a paper on *Forward Chaining in Higher Order
Logics* for a more complete exposition of chaining.

The *chainer* is implemented as a layer between the refiner
and the tactic definitions; it provides caching of the proofs
generated by the tactic. The goal of the chainer is two-fold:
maintain a cache of already-proved goals, so that tactics do not
have to repeat proofs; and provide a mechanism for chaining to
derive proofs that may be needed during interaction.

The chainer is implemented only for sequent calculi. Some examples
of typical forward chaining rules defined in the `ITT`
logic:

'A & 'B --> 'A
'A & 'B --> 'B
('A -> 'B) in Ui --> ('A in Ui)

The chainer works in the background, whenever the interactive
prover is waiting for input. If a proof is *found* by chaining,
the user is notified that a proof is available. Otherwise the
chainer does not affect the process of proving.

The chainer is implemented with an extended version of sequents,
containing the actual hypotheses presented to the user, and additional
hypotheses derived by forward chaining.