1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
<h2>What is Proof General?</h2>
<p>
<b>Proof General</b> is a generic interface for proof assistants,
currently based on the customizable text editor <i>Emacs</i>.
It works with either
<a href="http://www.xemacs.org/">XEmacs</a> or
<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>.
Proof General has been developed at the
<a href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a>
in the <a href="http://www.ed.ac.uk/">University of Edinburgh</a>.
</p>
<p>
To find out more, check the
<a href="features" features list</a>
and look at the
<a href="screenshot">screenshots</a>.
To get Proof General, visit the
<a href="download">download page</a>.
If you're not interested in interactive proof,
see the <a href="components">standalone components</a>
developed as part of Proof General.
To contact the developers, click
<?php hlink("feedback","here","Feedback form")?>.
</p>
<h2>What systems does Proof General work with?</h2>
<p>
Proof General comes ready-customized for these proof assistants:
</p>
<table width="90%">
<tr>
<td align="center">
<?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
"<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">",
"The Isabelle Home Page"); ?>
</td>
<td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for
<?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
"Isabelle", "The Isabelle Home Page"); ?>
<br>
<div style="font-size: smaller">
By
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
and
Markus Wenzel.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://pauillac.inria.fr/coq/",
"<img src=\"images/coqlogo4.gif\" width=66 height=61 border=0 alt=\"Coq badge\">","The Coq Home Page") ?>
</td>
<td>
<b><?php fileshow("ProofGeneral/coq/README","Coq Proof General "); ?></b> for
<?php hlink("http://pauillac.inria.fr/coq/",
"Coq","The Coq Home Page") ?>
<br>
<div style="font-size: smaller">
By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and
<a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html",
"<img src=\"images/phox-einstein.jpg\" width=80 height=48 border=0 alt=\"PhoX logo\">",
"The PhoX Home Page") ?>
</td>
<td><b><?php fileshow("ProofGeneral/phox/README","PhoX Proof General "); ?></b> for
<?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html",
"PhoX","The PhoX Home Page") ?>
<br>
<div style="font-size: smaller">
By
<a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a>
and
<a href="mailto:roziere@logique.jussieu.fr">Paul Roziere</a>.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://www.dcs.ed.ac.uk/home/lego",
"<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">",
"The LEGO Home Page") ?>
</td>
<td><b><?php fileshow("ProofGeneral/lego/README","LEGO Proof General "); ?></b> for
<?php hlink("http://www.dcs.ed.ac.uk/home/lego",
"LEGO","The LEGO Home Page") ?>
<br>
<div style="font-size: smaller">
By Thomas Kleymann, Dilip Sequeira,
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
and
<a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>.
</div>
</td>
</tr>
</table>
<p>
There are also <i>experimental</i> instances of Proof General:
<ul>
<li><b><?php fileshow("ProofGeneral/hol98/README","HOL Proof General"); ?></b>,
for <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL98</a>.
</li>
<li><b><?php fileshow("ProofGeneral/twelf/README","Twelf Proof General"); ?></b>,
for <a href="http://www.twelf.org">Twelf</a>.
</li>
<li><b><?php fileshow("ProofGeneral/acl2/README","ACL2 Proof General"); ?></b>,
for <a href="http://www.cs.utexas.edu/users/moore/acl2">ACL2</a>.
</li>
</ul>
<p>
These instances of Proof General are functional, but only show a bare
fraction of what is possible. We are
seeking volunteers to support and improve each of these
(please <a href="feedback">send a note to
<tt><?php print $project_feedback; ?></tt></a> if you're interested).
</p>
<p>
Proof General is ready to be customized to new proof assistants.
It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el",
"very easy"); ?> to get basic support working.
Full <a href="doc">documentation on
configuration</a> is provided.
</p>
|
