RelatedSystems < PG

PG Web>RelatedSystems (08 Sep 2006, HuaYang ) (raw view)EditAttach
---+!! Systems related to Proof General

%P% _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 [[http://www.cs.ru.nl/~freek/digimath/index.html][Freek Wiedijk's compendium]]
for that).

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

%TOC%


Apologies for somewhat ad hoc categorizations. 

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

---+++ Isabelle interfaces

   * [[http://homepages.inf.ed.ac.uk/da/Isamode/][Isamode]]<br/>
     uses XEmacs as the front-end and only work for Isabelle. <br/>
     _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. <br/>
     might be thought as the precedent of PG Emacs for Isabelle. <br/>
     not maintained <br/>

   * [[http://www.informatik.uni-bremen.de/~cxl/tas/][Isawin]]<br/>
     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. <br>
     proofs are constructed mainly by drag&drop. <br/>

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

---+++ Others

   * [[http://imps.mcmaster.ca/][IMPS]]<br/>
      Foundation based on simple type theory. <br/>
      Has an Emacs based interface and tools to output proof trees typeset in TeX.

   * !PVS<br/>
      Has an Emacs-based interface.  Manages proof obligations, supporting
      out-of-order development.

   * !ACL2<br/>
      Has an Emacs-based interface.

---++ Dependent type theory based provers


---+++ Coq interfaces

   * [[http://www-sop.inria.fr/croap/ctcoq/ctcoq-eng.html][CtCoq]]<br/>
     its GUI was developed using the [[http://www-sop.inria.fr/croap/centaur/centaur.html][Centaur]] system. <br/>
     runs on the machines with the X window system. <br/>
     features _proof-by-pointing_, _script management_ as well as _proofs' textual explanation_ <br/>
     replaced by PCoq
     
   * [[http://www-sop.inria.fr/lemme/pcoq/][PCoq]]<br>
     provides an interface developed in Java, therefore runs on any machine with the Java runtime environment. <br/>
     the first (probably the first) to introduce drag-and-drop manipulation of formulae. <br/>
     inherits most features of !CtCoq <br/>

---+++ Programming language-style

   * !Agda<br/>
      Has an Emacs-based interface supporting interactive refinement by replacing meta-variables with
      terms chosen from a menu generated by the system.

   * !Alfa<br/>
      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<br/>
      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<br/>
     centering around a knowledge base (called _library_), user interfaces are connected to the base as processes. <br/>
     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
Copyright © 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