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.
  not maintained
  

• Isawin
  provides a direct-manipulation-allowed GUI, where objects like proofs, theorems, tactics etc. are visualised by icons, thus accepts users without the knowledge of the prover's language.
  proofs are constructed mainly by drag&drop.
  

• 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.
  not maintained
  

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
  its GUI was developed using the Centaur system.
  runs on the machines with the X window system.
  features proof-by-pointing, script management as well as proofs' textual explanation
  replaced by PCoq

• PCoq
  provides an interface developed in Java, therefore runs on any machine with the Java runtime environment.
  the first (probably the first) to introduce drag-and-drop manipulation of formulae.
  inherits most features of CtCoq
  

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
  centering around a knowledge base (called library), user interfaces are connected to the base as processes.
  support multiple user working in parallel. Currently major user interfaces of NuPrl 5 include navigator, Emacs mode editors and the web front-end.