TWiki> PG Web>RelatedSystems (revision 1)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

  • Isawin


  • 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

  • PCoq

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


  • NuPrl

Edit | Attach | Print version | History: r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 05 Sep 2006 - 22:11:13 - 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