37 http://isabelle.in.tum.de/overview.html |
37 http://isabelle.in.tum.de/overview.html |
38 http://en.wikipedia.org/wiki/Isabelle_(theorem_prover) |
38 http://en.wikipedia.org/wiki/Isabelle_(theorem_prover) |
39 |
39 |
40 * IsarMathLib. |
40 * IsarMathLib. |
41 |
41 |
|
42 The goal of the project is to create a library of formalized mathematics, |
|
43 similar to the Mizar Mathematical Library, but written for the Isabelle/Isar |
|
44 theorem prover (ZF logic). |
|
45 |
|
46 See |
|
47 |
|
48 http://savannah.nongnu.org/projects/isarmathlib |
|
49 http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel |
|
50 |
|
51 ** http://isarmathlib.org/ |
|
52 |
42 This site is an experimental HTML rendering of fragments of the IsarMathLib |
53 This site is an experimental HTML rendering of fragments of the IsarMathLib |
43 project. IsarMathLib is a library of mathematical proofs formally verified by |
54 project. IsarMathLib is a library of mathematical proofs formally verified by |
44 the Isabelle theorem proving environment. The formalization is based on the |
55 the Isabelle theorem proving environment. The formalization is based on the |
45 Zermelo-Fraenkel set theory. |
56 Zermelo-Fraenkel set theory. |
46 |
57 |
|
58 ** Tiddly Formal Math. |
|
59 |
|
60 This site is an experimental TiddlyWiki rendering of fragments of the |
|
61 IsarMathLib project. IsarMathLib is a library of mathematical proofs formally |
|
62 verified by the Isabelle theorem proving environment. The formalization is |
|
63 based on the Zermelo-Fraenkel set theory. |
|
64 |
47 See |
65 See |
48 |
66 |
49 http://isarmathlib.org/ |
67 http://formalmath.tiddlyspot.com/ |