56
|
1 |
-*- outline -*-
|
|
2 |
|
|
3 |
* proofgeneral.
|
|
4 |
|
|
5 |
$ sudo apt-get install proofgeneral
|
|
6 |
$ sudo apt-get install proofgeneral-coq
|
|
7 |
$ sudo apt-get install proofgeneral-misc
|
|
8 |
$ sudo apt-get install proofgeneral-doc
|
|
9 |
$ sudo apt-get install proofgeneral-minlog
|
|
10 |
|
|
11 |
or build from source:
|
|
12 |
|
|
13 |
$ make clean
|
|
14 |
$ make compile EMACS=xemacs
|
|
15 |
$ cat ~/.emacs
|
|
16 |
...
|
|
17 |
(load-file "dir/generic/proof-site.el")
|
|
18 |
...
|
|
19 |
|
|
20 |
See
|
|
21 |
|
|
22 |
http://proofgeneral.inf.ed.ac.uk/
|
|
23 |
|
|
24 |
* Isabelle.
|
|
25 |
|
|
26 |
Isabelle is a generic proof assistant.
|
|
27 |
|
|
28 |
It allows mathematical formulas to be expressed in a formal language and
|
|
29 |
provides tools for proving those formulas in a logical calculus. The main
|
|
30 |
application is the formalization of mathematical proofs and in particular
|
|
31 |
formal verification, which includes proving the correctness of computer
|
|
32 |
hardware or software and proving properties of computer languages and
|
|
33 |
protocols.
|
|
34 |
|
|
35 |
See
|
|
36 |
|
|
37 |
http://isabelle.in.tum.de/overview.html
|
|
38 |
http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)
|
|
39 |
|
|
40 |
* IsarMathLib.
|
|
41 |
|
|
42 |
This site is an experimental HTML rendering of fragments of the IsarMathLib
|
|
43 |
project. IsarMathLib is a library of mathematical proofs formally verified by
|
|
44 |
the Isabelle theorem proving environment. The formalization is based on the
|
|
45 |
Zermelo-Fraenkel set theory.
|
|
46 |
|
|
47 |
See
|
|
48 |
|
|
49 |
http://isarmathlib.org/
|