diff options
Diffstat (limited to 'html/main.html')
| -rw-r--r-- | html/main.html | 146 |
1 files changed, 146 insertions, 0 deletions
diff --git a/html/main.html b/html/main.html new file mode 100644 index 00000000..499f7429 --- /dev/null +++ b/html/main.html @@ -0,0 +1,146 @@ +<h2>What is Proof General?</h2> +<p> +<b>Proof General</b> is a generic interface for proof assistants, +currently based on the customizable text editor <i>Emacs</i>. +It works with either +<a href="http://www.xemacs.org/">XEmacs</a> or +<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>. +Proof General has been developed at the +<a href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a> +in the <a href="http://www.ed.ac.uk/">University of Edinburgh</a>. +</p> +<p> +To find out more, check the +<a href="features"> features list</a> +and look at the +<a href="screenshot">screenshots</a>. +To get Proof General, visit the +<a href="download">download page</a>. +If you're not interested in interactive proof, +see the <a href="components">standalone components</a> +developed as part of Proof General. +To contact the developers, click +<?php hlink("feedback","here","Feedback form")?>. +</p> + + + +<h2>What systems does Proof General work with?</h2> + +<p>Proof General comes ready-to-go for these proof +assistants:</p> + +<table width="90%"> + <tr> + <td align="center"> + <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/", + "<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">", + "The Isabelle Home Page"); ?> + </td> + <td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for + <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/", + "Isabelle", "The Isabelle Home Page"); ?> + <br> + <div style="font-size: smaller"> + By + <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a> + and + Markus Wenzel. + </div> + </td> + </tr> + <tr> + <td align="center"> + <?php hlink("http://pauillac.inria.fr/coq/", + "<img src=\"images/coqlogo4.gif\" width=66 height=61 border=0 alt=\"Coq badge\">","The Coq Home Page") ?> + </td> + <td> + <b><?php fileshow("ProofGeneral/coq/README","Coq Proof General "); ?></b> for + <?php hlink("http://pauillac.inria.fr/coq/", + "Coq","The Coq Home Page") ?> + <br> + <div style="font-size: smaller"> + By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and + <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>. + </div> + </td> + </tr> + <tr> + <td align="center"> + <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html", + "<img src=\"images/phox-einstein.jpg\" width=80 height=48 border=0 alt=\"PhoX logo\">", + "The PhoX Home Page") ?> + </td> + <td><b><?php fileshow("ProofGeneral/phox/README","PhoX Proof General "); ?></b> for + <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html", + "PhoX","The PhoX Home Page") ?> + <br> + <div style="font-size: smaller"> + By + <a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a> + and + <a href="mailto:roziere@logique.jussieu.fr">Paul Roziere</a>. + </div> + </td> + </tr> + <tr> + <td align="center"> + <?php hlink("http://www.dcs.ed.ac.uk/home/lego", + "<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">", + "The LEGO Home Page") ?> + </td> + <td><b><?php fileshow("ProofGeneral/lego/README","LEGO Proof General "); ?></b> for + <?php hlink("http://www.dcs.ed.ac.uk/home/lego", + "LEGO","The LEGO Home Page") ?> + <br> + <div style="font-size: smaller"> + By Thomas Kleymann, Dilip Sequeira, + <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a> + and + <a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>. + </div> + </td> + </tr> +</table> + +<p>There are also <i>experimental</i> or <i>in-development</i> instances +of Proof General:</p> + +<ul> +<li><b><?php fileshow("ProofGeneral/hol98/README","HOL Proof +General"); ?></b>, for <a +href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL98</a>.</li> + +<li><b><?php fileshow("ProofGeneral/twelf/README","Twelf Proof +General"); ?></b>, for <a +href="http://www.twelf.org">Twelf</a>.</li> + +<li><b><?php fileshow("ProofGeneral/acl2/README","ACL2 Proof +General"); ?></b>, for <a +href="http://www.cs.utexas.edu/users/moore/acl2">ACL2</a>.</li> + +<li><b><?php fileshow("ProofGeneral/plastic/README","Plastic Proof +General"); ?></b>, for <a +href="http://www.dur.ac.uk/CARG/plastic.html">Plastic</a> +(in development).</li> + + +<li><b><?php fileshow("ProofGeneral/lclam/README","Lambda-Clam Proof +General"); ?></b>, for <a +href="http://dream.dai.ed.ac.uk/software/systems/lambda-clam/">Lambda-CLAM</a> +(in development).</li> +</ul> + +<p>The instances of Proof General marked "in development" above are +not considered complete, but are supported by the developers of proof +systems. The other instances above are "technology demonstrations" of +Proof General for other popular provers, but only show a bare fraction +of what is possible. We are seeking volunteers to support and improve +each of these (please <a href="feedback">send a note to <tt><?php +print $project_feedback; ?></tt></a> if you're interested).</p> + +<p>Proof General is ready to be customized to new proof assistants. +It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", +"very easy"); ?> to get basic support working. Full <a +href="ProofGeneral/doc/PG-adapting.pdf">documentation on +configuration</a> is provided.</p> |