author | Oleksandr Gavenko <gavenkoa@gmail.com> |
Wed, 17 Mar 2010 15:24:36 +0200 | |
changeset 347 | 8ae88e9dd05d |
parent 94 | db45445863c1 |
child 735 | 5c437e2d5fe1 |
permissions | -rw-r--r-- |
56 | 1 |
-*- outline -*- |
2 |
||
82 | 3 |
* Info/links. |
4 |
||
5 |
See |
|
6 |
||
7 |
http://en.wikipedia.org/wiki/Automated_theorem_proving |
|
8 |
||
9 |
||
56 | 10 |
* proofgeneral. |
11 |
||
12 |
$ sudo apt-get install proofgeneral |
|
13 |
$ sudo apt-get install proofgeneral-coq |
|
14 |
$ sudo apt-get install proofgeneral-misc |
|
15 |
$ sudo apt-get install proofgeneral-doc |
|
16 |
$ sudo apt-get install proofgeneral-minlog |
|
17 |
||
18 |
or build from source: |
|
19 |
||
20 |
$ make clean |
|
21 |
$ make compile EMACS=xemacs |
|
22 |
$ cat ~/.emacs |
|
23 |
... |
|
24 |
(load-file "dir/generic/proof-site.el") |
|
25 |
... |
|
26 |
||
27 |
See |
|
28 |
||
29 |
http://proofgeneral.inf.ed.ac.uk/ |
|
30 |
||
31 |
* Isabelle. |
|
32 |
||
33 |
Isabelle is a generic proof assistant. |
|
34 |
||
35 |
It allows mathematical formulas to be expressed in a formal language and |
|
36 |
provides tools for proving those formulas in a logical calculus. The main |
|
37 |
application is the formalization of mathematical proofs and in particular |
|
38 |
formal verification, which includes proving the correctness of computer |
|
39 |
hardware or software and proving properties of computer languages and |
|
40 |
protocols. |
|
41 |
||
42 |
See |
|
43 |
||
44 |
http://isabelle.in.tum.de/overview.html |
|
45 |
http://en.wikipedia.org/wiki/Isabelle_(theorem_prover) |
|
46 |
||
47 |
* IsarMathLib. |
|
48 |
||
70
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
49 |
The goal of the project is to create a library of formalized mathematics, |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
50 |
similar to the Mizar Mathematical Library, but written for the Isabelle/Isar |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
51 |
theorem prover (ZF logic). |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
52 |
|
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
53 |
See |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
54 |
|
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
55 |
http://savannah.nongnu.org/projects/isarmathlib |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
56 |
http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
57 |
|
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
58 |
** http://isarmathlib.org/ |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
59 |
|
56 | 60 |
This site is an experimental HTML rendering of fragments of the IsarMathLib |
61 |
project. IsarMathLib is a library of mathematical proofs formally verified by |
|
62 |
the Isabelle theorem proving environment. The formalization is based on the |
|
63 |
Zermelo-Fraenkel set theory. |
|
64 |
||
70
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
65 |
** Tiddly Formal Math. |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
66 |
|
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
67 |
This site is an experimental TiddlyWiki rendering of fragments of the |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
68 |
IsarMathLib project. IsarMathLib is a library of mathematical proofs formally |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
69 |
verified by the Isabelle theorem proving environment. The formalization is |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
70 |
based on the Zermelo-Fraenkel set theory. |
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
71 |
|
56 | 72 |
See |
73 |
||
70
7994c7089afb
Explain proof assistant.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
56
diff
changeset
|
74 |
http://formalmath.tiddlyspot.com/ |
82 | 75 |
|
94 | 76 |
* HOL Light. |
77 |
||
78 |
HOL Light is a computer program to help users prove interesting mathematical |
|
79 |
theorems completely formally in higher order logic. It sets a very exacting |
|
80 |
standard of correctness, but provides a number of automated tools and |
|
81 |
pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and |
|
82 |
real analysis) to save the user work. It is also fully programmable, so users |
|
83 |
can extend it with new theorems and inference rules without compromising its |
|
84 |
soundness. |
|
85 |
||
86 |
Ocalm. |
|
87 |
||
88 |
See |
|
89 |
||
90 |
http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html |
|
91 |
||
85 | 92 |
* ACL2. |
93 |
||
94 |
ACL2 (A Computational Logic for Applicative Common Lisp) is a software system |
|
95 |
consisting of a programming language, an extensible theory in a first-order |
|
96 |
logic, and a mechanical theorem prover. ACL2 is designed to support automated |
|
97 |
reasoning in inductive logical theories, mostly for the purpose of software |
|
98 |
and hardware verification. The input language and implementation of ACL2 are |
|
99 |
built on Common Lisp. ACL2 is free, open source (GPL) software. |
|
100 |
||
101 |
$ sudo apt-get install acl2 |
|
102 |
||
103 |
See |
|
104 |
||
105 |
http://www.cs.utexas.edu/users/moore/acl2/ |
|
106 |
http://en.wikipedia.org/wiki/ACL2 |
|
107 |
||
82 | 108 |
* PVS Specification and Verification System |
109 |
||
83 | 110 |
Old (1992). Many article in 199x. |
111 |
||
112 |
The system is implemented in Common Lisp, and is released under the GNU |
|
113 |
General Public License (GPL). |
|
82 | 114 |
|
115 |
See |
|
116 |
||
117 |
http://pvs.csl.sri.com/ |
|
118 |
http://en.wikipedia.org/wiki/Prototype_Verification_System |
|
119 |
http://www-formal.stanford.edu/clt/ARS/Entries/pvs |
|
120 |
||
121 |
* The TPTP Problem Library for Automated Theorem Proving. |
|
122 |
||
123 |
The TPTP (Thousands of Problems for Theorem Provers) is a library of test |
|
124 |
problems for automated theorem proving (ATP) systems. The TPTP supplies the |
|
125 |
ATP community with: |
|
126 |
||
127 |
* A comprehensive library of the ATP test problems that are available today, |
|
128 |
in order to provide an overview and a simple, unambiguous reference |
|
129 |
mechanism. |
|
130 |
* A comprehensive list of references and other interesting information for |
|
131 |
each problem. |
|
132 |
* Arbitrary size instances of generic problems (e.g., the N-queens problem). |
|
133 |
* A utility to convert the problems to existing ATP systems' formats. |
|
134 |
* General guidelines outlining the requirements for ATP system evaluation. |
|
135 |
* Standards for input and output for ATP systems. |
|
136 |
||
137 |
The principal motivation for the TPTP is to support the testing and evaluation |
|
138 |
of ATP systems, to help ensure that performance results accurately reflect the |
|
139 |
capabilities of the ATP system being considered. A common library of problems |
|
140 |
is necessary for meaningful system evaluations, meaningful system comparisons, |
|
141 |
repeatability of testing, and the production of statistically significant |
|
142 |
results. The TPTP is such a library. |
|
143 |
||
144 |
See |
|
145 |
||
146 |
http://www.cs.miami.edu/~tptp/ |
|
83 | 147 |
|
148 |
* SPASS. |
|
149 |
||
150 |
An Automated Theorem Prover for First-Order Logic with Equality. |
|
151 |
||
152 |
See |
|
153 |
||
154 |
http://www.spass-prover.org/index.html |
|
84
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
155 |
|
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
156 |
* Competition. |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
157 |
|
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
158 |
See |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
159 |
|
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
160 |
http://www.cs.miami.edu/~tptp/CASC/ |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
161 |
http://www.cs.albany.edu/~nvm/cade.html |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
162 |
|
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
163 |
* Conference. |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
164 |
|
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
165 |
IJCAR is a series of conferences on the topics of automated reasoning, |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
166 |
automated deduction, and related fields. It is organized semi-regularly as a |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
167 |
merger of other meetings. IJCAR replaces those independent conferences in the |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
168 |
years it takes place. The conference is organized by CADE Inc., and CADE has |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
169 |
always been one of the conferences partaking in IJCAR. |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
170 |
|
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
171 |
See |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
172 |
|
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
173 |
http://www.ijcar.org/ |
366b2a8bafe6
Conference & competition.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
83
diff
changeset
|
174 |
http://en.wikipedia.org/wiki/International_Joint_Conference_on_Automated_Reasoning |
94 | 175 |
|
176 |
* Top 100. |
|
177 |
||
178 |
http://www.cs.ru.nl/~freek/100/ |
|
179 |
(winner) |
|
180 |
http://personal.stevens.edu/~nkahl/Top100Theorems.html |
|
181 |
(orig list) |
|
182 |
http://www.cse.unsw.edu.au/~kleing/top100/#5 |
|
183 |
(Isabelle) |