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
|
<h2>Manual</h2>
<p>
Here is the
<?php htmlshow("ProofGeneral-3.1/doc/ProofGeneral_toc.html","Proof General user manual","Proof General Manual") ?> in HTML form, as included in the distribution.
<br>
For printing you can download the
<?php download_link("ProofGeneral-3.1/doc/ProofGeneral.ps.gz", "gzipped ps file") ?>
(recommended) or the
<?php download_link("ProofGeneral-3.1/doc/ProofGeneral.pdf", "pdf file") ?>.
</p>
<p>
The manual (in HTML and Info formats), as well as other documentation,
is included in the <?php link_root("download","download.") ?> 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.phtml">mailing
list</a>.
</p>
<h2>References</h2>
<p> Ideas for the future of Proof General are given here:
</p>
<ul>
<li><a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>.
<b><i>Protocols for Interactive e-Proof</i></b>.
Draft version, see
<a href="http://zermelo.dcs.ed.ac.uk/home/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.dcs.ed.ac.uk/lfcsreps/EXPORT/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>
|
