+
−-*- 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/