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.