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