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
|
<h2>Manual</h2>
<p>
There are two manuals for Proof General:
</p>
<ul>
<li> the
<?php htmlshow("ProofGeneral-3.3/doc/ProofGeneral_toc.html","Proof General user manual ","Proof General Manual") ?>
</li>
<li> the
<?php htmlshow("ProofGeneral/doc/PG-adapting_toc.html","Adapting Proof General manual","Adapting Proof General manual") ?>
</li>
</ul>
<p>
The second manual gives instructions on how to adapt Proof General to new
proof systems, it's not needed for ordinary use.
</p>
<p>
For printing you can download:
<ul>
<li>
<?php download_link("ProofGeneral-3.3/doc/ProofGeneral.ps.gz", "User manual [ps]") ?> and
<?php download_link("ProofGeneral-3.3/doc/PG-adapting.ps.gz", "Adapting manual [ps]") ?>, or
</li>
<li>
<?php download_link("ProofGeneral-3.3/doc/ProofGeneral.pdf", "User manual [pdf]") ?>,
<?php download_link("ProofGeneral-3.3/doc/PG-adapting.pdf", "Adapting manual [pdf]") ?>
</li>
</ul>
<p>
The PostScript files are recommended over the PDF.
</p>
<p>
Note that both manuals (in HTML and Info formats) are included in the
<a href="download">download</a>. When running Proof General the manual
is available from the "Proof General" menu. It should also appear in
the system Info pages.
</p>
<p>
You can discuss Proof General with other users and receive
announcements by joining our <a href="mailinglist.html">mailing
list</a>.
</p>
<h2>References</h2>
<p> Ideas for the future of Proof General are given here:
</p>
<ul>
<li><a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
<b><i>Protocols for Interactive e-Proof</i></b>.
Draft version, see
<a href="http://zermelo.dcs.ed.ac.uk/~da/drafts/#eproof">here</a>.
</li>
<li><a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>.
<b><i>Proof General Kit (white paper)</i></b>.
Draft version, see
<a href="http://zermelo.dcs.ed.ac.uk/home/da/drafts/#white">here</a>.
</li>
</ul>
<p> A technology overview of Proof General is given here:
</p>
<ul>
<li> <a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>.
<a href="papers/pgoutline.ps.gz">Proof General: A Generic Tool for
Proof Development</a>.
<i>Tools and Algorithms for the Construction and
Analysis of Systems, Proc TACAS 2000</i>, LNCS 1785.
<br>
Here are some <a href="papers/pgtalk.pdf">slides</a>
used for this talk and some other presentations of Proof General.
</li>
</ul>
<p> Proof General supports Script Management as documented in:
</p>
<ul>
<li> <a
href="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves
Bertot</a> and <a
href="http://www.inria.fr/croap/personnel/Laurent.Thery/me.html">Laurent
Théry</a>. <a
href="ftp://babar.inria.fr/pub/croap/bertot/jsymcomp.ps">A
generic approach to building user interfaces for theorem
provers</a>.
<i>Journal of Symbolic Computation</i>, 25(7), pp. 161-194, February 1998.
</li>
</ul>
<p>
It has support for Proof by Pointing, as documented in:
</p>
<ul>
<li> <A
HREF="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves
Bertot</A>, <A HREF="http://www.dcs.ed.ac.uk/home/tms">
Thomas Kleymann-Schreiber</A> and <A
HREF="http://www.dcs.ed.ac.uk/home/djs">Dilip Sequeira</a>.
<I>Implementing Proof by Pointing without a Structure Editor</I>.
LFCS Technical Report <A
HREF="http://www.lfcs.informatics.ed.ac.uk/reports/97/ECS-LFCS-97-368/index.html">ECS-LFCS-97-368</a>.
Also published as Rapport de recherche de l'INRIA
<A HREF="http://www.inria.fr/Unites/SOPHIA-eng.html"> Sophia
Antipolis</a> <A
HREF="http://www.inria.fr/RRRT/RR-3286.html">RR-3286</a>
</li>
</ul>
|
