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
|
<h2>Related projects</h2>
<p>
Here are some links to related things.
If you have any suggestions
for links to include here, please
<?php hlink("feedback.phtml","contact us","Feedback form")?>.
</p>
<ul>
<li><a href="http://zermelo.dcs.ed.ac.uk/~isamode">Isamode</a>
is an XEmacs front-end for Isabelle. It has a different
feature collection compared with Proof General:
script management is not supported, but there are extensive
menus and shortcuts provided for common Isabelle
commands.
</li>
</ul>
<ul>
<li><a href="http://www-sop.inria.fr/croap/ctcoq/ctcoq-eng.html">CtCoq</a>
is an interface for the Coq theorem prover, developed
at INRIA, Sophia Antipolis, as part of
<a href="http://www-sop.inria.fr/croap/">Projet CROAP</a>.
Like Proof General, CtCoq is based on a general approach for
building user-interfaces for theorem provers, although no other
current theorem provers are supported. Unlike Proof General, CtCoq
is based on a graphical environment with structure editing,
created with the <a
href="http://www-sop.inria.fr/croap/centaur/centaur.html">Centaur</a>
system.
</li>
</ul>
<ul>
<li>
<a href="http://www.ags.uni-sb.de/~omega/">OMEGA</a> is
a collection of web-based distributed tools for supporting
theorem proving.
</li>
</ul>
<ul>
<li>
<a href="http://www.dcs.gla.ac.uk/prosper/">Prosper</a> is a project
to develop an extensible, open proof tool architecture for
incorporating formal verification into industrial CAD/CASE tool
flows and design methodologies. The tools include novel
user-friendly interfaces.
</li>
</ul>
<ul>
<li>
As a possible foundation for generic proof environments,
<a href="http://www.nag.co.uk/projects/openmath/omsoc/">OpenMath</a>
is a standard representation form for mathematical objects, which
links in with the <a href="http://www.w3.org/Math/">MathML</a>
markup language.
</li>
</ul>
<ul>
<li>
<a href="http://www.mrg.dist.unige.it/omrs/index.html">Open Mechanized Reasoning System (OMRS)</a>
</li>
</ul>
<ul>
<li>
<a href="http://www.cs.unibo.it/~asperti/HELM/home.html">Hypertextual Electronic Library of Mathematics (HELM)</a>
</li>
</ul>
<ul>
<li>
<a href="http://eti.cs.uni-dortmund.de:8080/servlet/ETI">ETI</a>
</li>
</ul>
|
