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="wide">
  31
  32         <li> the user interface sports high quality bidimensional rendering of
  33         proofs and formulae transformed on-the-fly to
  34         <a href="http://www.w3.org/Math/">MathML</a> markup, on which direct
  35         manipulation of the underlying CIC terms is still possible; </li>
  36
  37         <li> the knowledge base is distributed: every authored concepts can be
  38         published becoming part of the Matita library which can be browsed as
  39         an hypertext (locally or on the World Wide Web) and searched by means
  40         of content-based queries; </li>
  41
  42         <li> the tactical language, part of the proof language, has
  43         step-by-step semantics, enabling inspection and replaying of deeply
  44         structured proof scripts. </li>
  45
  46       </ul>
  47
  48       <!--#include virtual="bottombar.shtml" -->
  49     </div>
  50   </body>
  51 </html>