faq for thunderbird.
-*- outline -*-
* proofgeneral.
$ sudo apt-get install proofgeneral
$ sudo apt-get install proofgeneral-coq
$ sudo apt-get install proofgeneral-misc
$ sudo apt-get install proofgeneral-doc
$ sudo apt-get install proofgeneral-minlog
or build from source:
$ make clean
$ make compile EMACS=xemacs
$ cat ~/.emacs
...
(load-file "dir/generic/proof-site.el")
...
See
http://proofgeneral.inf.ed.ac.uk/
* Isabelle.
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. The main
application is the formalization of mathematical proofs and in particular
formal verification, which includes proving the correctness of computer
hardware or software and proving properties of computer languages and
protocols.
See
http://isabelle.in.tum.de/overview.html
http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)
* IsarMathLib.
This site is an experimental HTML rendering of fragments of the IsarMathLib
project. IsarMathLib is a library of mathematical proofs formally verified by
the Isabelle theorem proving environment. The formalization is based on the
Zermelo-Fraenkel set theory.
See
http://isarmathlib.org/