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