A Parameterized Proof Manager

Proof management is an important issue for interactive theorem provers. We describe a simple proof manager that derives a large measure of its power from being parameterized by structures that separately manage 1) proof-specific information and 2) the relationships between proofs. Examples of its use include mixed forward and backward proof, automatic proof logging and replay, support for documenting a proof either before, during, or after the proof effort, and the management of proof dependencies.

paper