+<!-- $Id$ -->
<!--#include virtual="xhtml-header.shtml" -->
<html>
- <head>
- <title>Matita home page</title>
- </head>
- <style>
- a {text-decoration:none}
- img.image{ display: none; }
+ <head>
+ <title>Matita - Home Page</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+ </head>
+ <body>
+ <!--#include virtual="menubar.shtml" -->
+ <div class="main">
- dl#matitaMap {
- margin-left:auto;
- margin-right:auto;
- margin-top:50px;
- padding: 0;
- background: url(images/matita.png) top left no-repeat;
- height: 590px;
- width: 485px;
- position: relative;
- }
-
- dt{ margin: 0; padding: 0; position: absolute; font-size: 85%; display: none; }
- dd{ margin: 0; padding: 0; position: absolute; font-size: 85%; }
-
- dd#developersDef{ top: 206px; left: 30px; }
- dd#developersDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
- dd#developersDef a span{ display: none; }
- dd#developersDef a:hover{ position: absolute; background: transparent url(images/bg0.png) ; top: 0px}
-
- dd#documentationDef{ top: 277px; left: 30px; }
- dd#documentationDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
- dd#documentationDef a span{ display: none; }
- dd#documentationDef a:hover{ position: absolute; background: transparent url(images/bg1.png) ; top: 0px}
-
- dd#communityDef{ top: 348px; left: 30px; }
- dd#communityDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
- dd#communityDef a span{ display: none; }
- dd#communityDef a:hover{ position: absolute; background: transparent url(images/bg2.png) ; top: 0px}
-
- dd#downloadDef{ top: 419px; left: 30px; }
- dd#downloadDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
- dd#downloadDef a span{ display: none; }
- dd#downloadDef a:hover{ position: absolute; background: transparent url(images/bg3.png) ; top: 0px}
+ <div class="topimage">
+ <img src="images/matita-text-big.png" alt="Big Matita label" />
+ </div>
- div#ex {margin-left:auto; margin-right:auto}
- </style>
+ <p> Matita is a new document-centric interactive theorem prover that
+ integrates several <a href="http://www.mkm-ig.org">Mathematical Knowledge
+ Management</a> tools and techniques. </p>
- <body>
+ <p>
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-matita.png">
+ <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
+ </a>
+ </span>
+ Matita is <strong>traditional</strong>. Its logical foundation is the
+ Calculus of (Co)Inductive Constructions (CIC). It can re-use
+ mathematical concepts produced by other proof assistants like
+ <a href="http://coq.inria.fr">Coq</a> and encoded in an
+ <a href="http://www.w3.org/XML/">XML</a> encoding of CIC. The interaction
+ paradigm of Matita is familiar, being inspired by CtCoq and
+ <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>. Its
+ proof language is procedural in the same spirit of LCF. </p>
+
+ <p> Matita is <strong>innovative</strong>: </p>
+ <ul>
-<div id="ex" >
-<img src="images/matita.png" width="485" height="590" border="0" class="image" />
+ <li>
+ <p>
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-matita-href.png">
+ <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
+ </a>
+ <a class="quiet" href="images/screenshot-matita-selection.png">
+ <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
+ </a>
+ </span>
+ the user interface sports high quality bidimensional rendering of
+ proofs and formulae transformed on-the-fly to <a
+ href="http://www.w3.org/Math/">MathML</a> markup, on which direct
+ manipulation of the underlying CIC terms is still possible;
+ </p>
+ </li>
- <dl id="matitaMap">
- <dt id="developers">1. Developers</dt>
- <dd id="developersDef"><a href="developers.shtml"></a></dd>
- <dt id="documentation">2. Documentation</dt>
- <dd id="documentationDef"><a href="documentation.shtml"></a></dd>
- <dt id="community">3. Community</dt>
- <dd id="communityDef"><a href="community.shtml"></a></dd>
- <dt id="download">4. Download</dt>
- <dd id="downloadDef"><a href="download.shtml"></a></dd>
- </dl>
- <div>
-
+ <li>
+ <p>
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
+ <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
+ </a>
+ <a class="quiet" href="images/screenshot-cicbrowser-query.png">
+ <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
+ </a>
+ <!--
+ <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
+ <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering" />
+ </a>
+ -->
+ </span>
+ the knowledge base is distributed: every authored concepts can be
+ published becoming part of the Matita library which can be <a
+ href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
+ (locally or on the World Wide Web) and <a
+ href="http://helm.cs.unibo.it/whelp/"> searched by means of
+ content-based queries</a>; </p>
+ </li>
+
+ <li>
+ <p>
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-tinycals.png">
+ <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
+ </a>
+ </span>
+ the tactical language, part of the proof language, has
+ step-by-step semantics, enabling inspection and replaying of deeply
+ structured proof scripts. </p>
+ </li>
+
+ </ul>
+
+ <!--#include virtual="bottombar.shtml" -->
+ </div>
</body>
</html>
-<!-- $Id$ -->
projects / helm.git / blobdiff