Footnotes

(1)

A proof assistant is a computerized helper for developing mathematical proofs. For short, we sometimes call it a prover, although we always have in mind an interactive system rather than a fully automated theorem prover.

(2)

A proof script is a sequence of commands which constructs a proof, usually stored in a file.

(3)

Some proof assistants provide some level of support for switching between multiple concurrent proofs, but Proof General does not use this. Generally the exact context for such proofs is hard to define to easily split them into multiple files.

(4)

In fact, this is an unnecessary restriction imposed by the original design of Proof General. There is nothing to stop future versions of Proof General allowing the queue region to be extended or shrunk, whilst the prover is processing it. Proof General 3.0 already relaxes the original design, by allowing successive assertion commands without complaining.

(5)

The suffix may depend of the specific proof assistant you are using e.g, Coq’s proof script files have to end with ‘.v’.

(6)

For example, LEGO generated additional compiled (optimised) proof script files for efficiency.

---

This document was generated on April 25, 2024 using texi2html 1.82.