Interface Concepts (Glossary)

REFACTOR please help extend this glossary

This page introduces some of the terminology used in the Proof General documentation.

Theorem Prover

A tool for constructing machine-assisted formal proofs. See SupportedProvers for details on the provers supported by Proof General.

Script Management (aka Proof Scripting)

Interactive increpemental processing of proofs, similar in spirit to interactive step-debugging. Usually tailored to linear scripts. Definitions and proofs are contained in ProofScripts which are held in files. These scripts can be interactively 'executed', by sending them to the prover line by line. Proof General has tape-recorder style buttons which can be used to move the point of next-execution through a script. This is called proof scripting. It helps you to develop and debug proofs.

Locked Region

As you process a script, it becomes locked. Locked regions cannot usually be edited. This is a feature of Script Management that protects against breaking a proof by editing earlier sections/theories. To unlock locked regions, use the ''goto'', ''undo'', ''retract script'' or ''restart prover'' commands as appropriate.

Advanced users who want to allow editing of locked regions (risking loss of synchronisation) can set an interface option to allow this.


The communication protocol used by Proof General to work with the prover. This was designed by abstracting from the protocol used in the original ProofGeneralEmacs, and unifying differences exhibited by different theorem provers. See: PGIP.

Topic revision: r3 - 02 Oct 2006 - 21:46:17 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies