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
|
<?php
require('functions.php3');
small_header("Proof General Screenshots");
?>
<p>
Here are some screenshots of Proof General running with
different theorem provers. To see the full-size version
of a picture, click on its thumbnail.
</p>
<p>
<i>(NB: Your browser needs PNG support to view these pictures)</i>
</p>
<!-- todo: php3 this, add space between rows! -->
<table width="80%">
<tr>
<td width="200">
<a href="images/pg-lego-screenshot.png">
<img src="images/pg-lego-thumb.png" alt="LEGO Proof General" width=128 height=109 border=0>
</a>
</td>
<td>
<p>
Building a simple proof in LEGO with proof-by-pointing.
<br>
The top half of the window displays the proof script.
The bottom displays the output from LEGO at each
stage of the proof. Here, it shows
the current subgoals to be solved.
The part of the proof already processed by LEGO
has a blue background.
<br>
Clicking on terms in the subgoals list generates
commands which are added to the proof script.
</p>
</tr>
<tr>
<td width="200">
<a href="images/pg-coq-screenshot.png">
<img src="images/pg-coq-thumb.png" alt="Coq Proof General" width=153 height=115 border=0>
</a>
</td>
<td>
<p>
Coq Proof General running in multiple frame mode,
full screen shot (1024x768).
<br>
There are separate windows on the screen
for the script, goals, and response buffers.
In this picture, you can see Proof General's
indication that Coq is processing the
induction step, because the background of
the proof step is pink. It will become
blue when Coq finishes that step.
</p>
</tr>
<tr>
<td width="200">
<a href="images/pg-isa-screenshot.png">
<img src="images/pg-isa-thumb.png" alt="Isabelle Proof General" width=150 height=142 border=0>
</a>
</td>
<td>
<p>
Replaying a domain theory proof in Isabelle's HOLCF logic.
<br>
In Isabelle, theory files as well as ML files are coloured.
Proof General has some functions for processing and
undoing theory files, but most operations it provides
are for writing proof scripts in ML files.
<br>
Isabelle supports input and output in tokens which
display as symbols using the
<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol">X-Symbol</a>
package in conjunction with Proof General.
Here you can see some symbols in Isabelle's output.
</p>
</tr>
<tr>
<td width="200">
<a href="images/pg-isar-screenshot.png">
<img src="images/pg-isar-thumb.png" alt="Isabelle/Isar Proof General" width=150 height=142 border=0>
</a>
</td>
<td>
<p>
Replaying a proof in Isar, Isabelle's new proof language
developed by Markus Wenzel.
</p>
</tr>
<tr>
<td width="200">
<a href="images/pg-lego-console.png">
<img src="images/pg-lego-console-thumb.png" alt="LEGO Proof General (console)" width=174 height=65 border=0>
</a>
</td>
<td>
<p>
LEGO Proof General running in plain console mode.
<br>
This shows that you can run Proof General even if sometimes
you need to use a plain tty or xterminal. Of course, the
graphical features are reduced!
</p>
</tr>
</table>
<p>
For more pictures, see the Proof General <a href="gallery.phtml">gallery</a>.
</p>
<?php
click_to_go_back();
footer();
?>
|
