TheoremProverIsabelle < PG

PG Web>TheoremProvers>TheoremProverIsabelle (21 Aug 2006, DavidAspinall) (raw view)EditAttach

---+ 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 distingu\
ishing 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 re\
cent addition to Isabelle, so you need an up-to-date version.''' You can test whether your version supports PG/Eclipse by runni\
ng 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

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