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