helm/www/matita/matita.shtml

   1 <!--#include virtual="xhtml-header.shtml" -->
   2 <html>
   3   <head>
   4     <title>Matita - Home Page</title>
   5     <!--#include virtual="xhtml-meta.shtml" -->
   6   </head>
   7   <body>
   8     <!--#include virtual="menubar.shtml" -->
   9     <div class="main">
  10
  11       <div class="topimage">
  12         <img src="images/matita-text-big.png" />
  13       </div>
  14
  15       <p> Matita is a new document-centric interactive theorem prover that
  16       integrates several <a href="http://www.mkm-ig.org">Mathematical Knowledge
  17         Management</a> tools and techniques. </p>
  18
  19       <p> Matita is <strong>traditional</strong>. Its logical foundation is the
  20       Calculus of (Co)Inductive Constructions (CIC), and it can re-use
  21       mathematical concepts produced by other proof assistants like
  22       <a href="http://coq.inria.fr">Coq</a> and encoded in an
  23       <a href="http://www.w3.org/XML/">XML</a> dialect. The interaction
  24       paradigm of Matita is well known, having been inspired by
  25       <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>, and its
  26       proof language is procedural in the same spirit of LCF. </p>
  27
  28       <p> Matita is <strong>innovative</strong>: </p>
  29       <ul class="wide">
  30
  31         <li> its user interface sports high quality bidimensional rendering of
  32         proofs and formulae exploiting
  33         <a href="http://www.w3.org/Math/">MathML</a> markup, equipped with
  34         direct manipulation of the underlying CIC terms; </li>
  35
  36         <li> its library is distributed: every authored concepts can be
  37         published and become part of the Matita library which can be browsed as
  38         an hypertext (locally or on the World Wide Web) and searched by means of
  39         content-based queries; </li>
  40
  41         <li> the tactical language, part of the proof language, has
  42         step-by-step semantics, enabling inspection and replaying of deeply
  43         structured proof scripts </li>
  44
  45       </ul>
  46
  47       <!--#include virtual="bottombar.shtml" -->
  48     </div>
  49   </body>
  50 </html>
  51 <!-- $Id$ -->