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 Emacs.
It 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>.
Proof General
works best under
<a href="http://www.xemacs.org/">XEmacs</a>, but can also be used with
<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>.
You need a recent version in either case.
</p>
<p>
To read more about what Proof General
is and what it provides,
<a href="features">check the features list</a>.
To see what Proof General looks like in use, have a look at these
<a href="screenshot">screenshots</a>.
To download Proof General, visit the
<a href="download">download page</a>.
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="ProofGeneral/doc/PG-adapting.pdf">documentation on
configuration</a> is provided.
</p>
|
