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.
    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.
Topic revision: r3 - 08 Sep 2006 - 00:16:53 - 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