helm/www/matita/matita.shtml

   1 <!-- $Id$ -->
   2 <!--#include virtual="xhtml-header.shtml" -->
   3 <html>
   4   <head>
   5     <title>Matita - Home Page</title>
   6     <!--#include virtual="xhtml-meta.shtml" -->
   7   </head>
   8   <body>
   9     <!--#include virtual="menubar.shtml" -->
  10     <div class="main">
  11
  12       <div class="topimage">
  13         <img src="images/matita-text-big.png" alt="Big Matita label" />
  14       </div>
  15
  16       <p> Matita is a new document-centric interactive theorem prover that
  17       integrates several <a href="http://www.mkm-ig.org">Mathematical Knowledge
  18         Management</a> tools and techniques. </p>
  19
  20       <p> Matita is <strong>traditional</strong>. Its logical foundation is the
  21       Calculus of (Co)Inductive Constructions (CIC). It can re-use
  22       mathematical concepts produced by other proof assistants like
  23       <a href="http://coq.inria.fr">Coq</a> and encoded in an
  24       <a href="http://www.w3.org/XML/">XML</a> encoding of CIC. The interaction
  25       paradigm of Matita is familiar, being inspired by CtCoq and
  26       <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>. Its
  27       proof language is procedural in the same spirit of LCF. </p>
  28
  29       <p> Matita is <strong>innovative</strong>: </p>
  30       <ul class="with_screenshots">
  31
  32         <li>
  33         <p>
  34         <span class="screenshots">
  35           <a class="quiet" href="images/screenshot-matita-href.png">
  36             <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
  37           </a>
  38           <a class="quiet" href="images/screenshot-matita-selection.png">
  39             <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
  40           </a>
  41         </span>
  42         the user interface sports high quality bidimensional rendering of
  43         proofs and formulae transformed on-the-fly to <a
  44           href="http://www.w3.org/Math/">MathML</a> markup, on which direct
  45         manipulation of the underlying CIC terms is still possible;
  46         </p>
  47         </li>
  48
  49         <li>
  50         <p>
  51         <span class="screenshots">
  52           <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
  53             <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
  54           </a>
  55           <a class="quiet" href="images/screenshot-cicbrowser-query.png">
  56             <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
  57           </a>
  58           <!--
  59           <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
  60             <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering" />
  61           </a>
  62           -->
  63         </span>
  64         the knowledge base is distributed: every authored concepts can be
  65         published becoming part of the Matita library which can be <a
  66           href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
  67         (locally or on the World Wide Web) and <a
  68           href="http://helm.cs.unibo.it/whelp/"> searched by means of
  69           content-based queries</a>; </p>
  70         </li>
  71
  72         <li>
  73         <p>
  74         <span class="screenshots">
  75           <a class="quiet" href="images/screenshot-tinycals.png">
  76             <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
  77           </a>
  78         </span>
  79         the tactical language, part of the proof language, has
  80         step-by-step semantics, enabling inspection and replaying of deeply
  81         structured proof scripts. </p>
  82         </li>
  83
  84       </ul>
  85
  86       <!--#include virtual="bottombar.shtml" -->
  87     </div>
  88   </body>
  89 </html>