The Isabelle Theorem Prover

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus (including higher order logic). In comparison to similar systems, its distinguishing features are lots of flexibility and a good user base. Drawbacks are a steep learning curve, and an arcane syntax (well: the preferred Isar syntax isn't too bad; unfortunately proof scripts often mix in all manner of older syntax).

It is currently the only system configured to work with Proof General / Eclipse. '''Support for Proof General / Eclipse is a recent addition to Isabelle, so you need an up-to-date version.''' You can test whether your version supports PG/Eclipse by running the command {{{isabelle -I -X}}}. On a suitably modern release, this will cause Isabelle to respond in xml. Isabelle2005 is the first suitable ordinary release.

Isabelle (& its documentation) can be freely downloaded from: http://isabelle.in.tum.de/ Installation is easy for Linux and Mac OS systems, and possible but tricky for Windows systems.

(DanielWinterstein , 2005)

Topic revision: r1 - 21 Aug 2006 - 14:14:49 - 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