Systems related to Proof General

in progress

Here are some pointers to systems related to Proof General and brief notes on their features.

We're mainly interested in well known theorem proving systems/interfaces or those with notable facilities rather than a complete list (see Freek Wiedijk's compendium for that).

For us, notable facilities are those at the interface/presentation/manipulation levels.

Apologies for somewhat ad hoc categorizations.

Set theory, simple type-theory, LCF/HOL provers

Isabelle interfaces

• Isamode
  uses XEmacs as the front-end and only work for Isabelle.
  mode in the name implies a theory file mode for editing, and an Isabelle interaction mode for interacting with Isabelle making use of three buffers, a buffer for the proof state, a buffer for the Isabelle shell and a buffer for the current theory.
  might be thought as the precedent of PG Emacs for Isabelle.

• Isawin

• XIsabelle
  provides a graphical interface to Isabelle, implemented in Tcl/Tk and the program Expect.
  used for generating Latex files of proof trees.
  many content panes visible in the interface, that makes the display look complicated for the users.
  

Others

• IMPS
  Foundation based on simple type theory.
  Has an Emacs based interface and tools to output proof trees typeset in TeX .

• PVS
  Has an Emacs-based interface. Manages proof obligations, supporting out-of-order development.

• ACL2
  Has an Emacs-based interface.

Dependent type theory based provers

Coq interfaces

• CtCoq

• PCoq

Programming language-style

• Agda
  Has an Emacs-based interface supporting interactive refinement by replacing meta-variables with terms chosen from a menu generated by the system.

• Alfa
  A very beautful interface for Agda based on pretty-printing input scripts with proper typeset output. Uses custom Haskell toolkit (fudgets). Sadly no longer supported/available.

• Epigram
  Really meant as a language for programming rather than a language for proving. Has 2D based layout for presenting and editing inference rules. Emacs based interface at present(?).

Others

• NuPrl