aboutsummaryrefslogtreecommitdiffhomepage
path: root/html/links.phtml
blob: 4337d6380e56af5b823697352dd6e6bd8be402d2 (plain)
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
<p>
Here are some links to related things.  
<br>
If you have any suggestions 
for links to include here, or find broken links, 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://eti.cs.uni-dortmund.de:8080/servlet/ETI">ETI</a>
</li>
</ul>