TWiki> PG Web>RelatedSystems (revision 2)EditAttach

Systems related to Proof General

REFACTOR 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.


  • 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

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(?).


  • NuPrl
Edit | Attach | Print version | History: r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r2 - 06 Sep 2006 - 22:07:24 - HuaYang
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