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