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
134
135
136
137
138
139
140
141
142
143
144
145
|
<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-to-go 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://homepages.inf.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://homepages.inf.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> or <i>in-development</i> instances
of Proof General:</p>
<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>
<li><b><?php fileshow("ProofGeneral/plastic/README","Plastic Proof
General"); ?></b>, for <a
href="http://www.dur.ac.uk/CARG/plastic.html">Plastic</a>
(in development).</li>
<li><b><?php fileshow("ProofGeneral/lclam/README","Lambda-Clam Proof
General"); ?></b>, for <a href="http://dream.dai.ed.ac.uk/software/lambda-clam/">Lambda-CLAM</a>
(in development).</li>
</ul>
<p>The instances of Proof General marked "in development" above are
not considered complete, but are supported by the developers of proof
systems. The other instances above are "technology demonstrations" of
Proof General for other popular provers, 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="ProofGeneral/doc/PG-adapting.pdf">documentation on
configuration</a> is provided.</p>
|
