helm/www/matita/matita.shtml

   1 <!--#include virtual="xhtml-header.shtml" -->
   2 <!-- $Id$ -->
   3 <html xmlns="http://www.w3.org/1999/xhtml">
   4   <head>
   5     <meta name="keywords" content="Matita, prover, assistant" />
   6     <title>Matita - Home Page</title>
   7     <!--#include virtual="xhtml-meta.shtml" -->
   8   </head>
   9   <body>
  10     <!--#include virtual="menubar.shtml" -->
  11     <!--#include virtual="news.shtml" -->
  12     <div class="main">
  13
  14       <div class="topimage">
  15         <img src="images/matita-text-big.png" alt="Matita" />
  16         <a href="matita_it.shtml">
  17          <img src="flags/wit.gif" alt="italian flag" />
  18         </a>
  19       </div>
  20
  21       <p class="spaced">
  22       Matita (that means <em>pencil</em> in italian) is an experimental,
  23         interactive theorem prover under development at the
  24       <a href="http://www.cs.unibo.it">Computer Science Department</a> of the
  25       <a href="http://www.unibo.it">University of Bologna</a>.
  26       </p>
  27
  28 <!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
  29
  30       <p class="spaced">
  31       <span class="screenshots">
  32         <a class="quiet" href="images/screenshot-matita.png">
  33           <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
  34         </a>
  35       </span>
  36
  37       Matita is based on the
  38       Calculus of (Co)Inductive Constructions, and is compatible, at some
  39       extent, with <a href="http://coq.inria.fr">Coq</a>.
  40       It is a reasonably small and simple application, whose
  41       architectural and software complexity is meant to be mastered by
  42       students, providing a tool particularly suited for testing innovative
  43       ideas and solutions.
  44       Matita adopts a tactic based editing mode; (XML-encoded) proof objects
  45       are produced for storage and exchange.
  46       </p>
  47
  48       <p class="spaced">
  49       <span class="screenshots">
  50           <a class="quiet" href="images/screenshot-matita-href.png">
  51             <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
  52           </a>
  53           <a class="quiet" href="images/screenshot-matita-selection.png">
  54             <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
  55           </a>
  56         </span>
  57       The graphical interface has been inspired by CtCoq and
  58       <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
  59       It supports high quality bidimensional rendering of
  60       proofs and formulae transformed on-the-fly to
  61       <a href="http://www.w3.org/Math/">MathML</a> markup</p>
  62
  63       <p class="spaced">
  64       <span class="screenshots">
  65           <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
  66             <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
  67           </a>
  68           <a class="quiet" href="images/screenshot-cicbrowser-query.png">
  69             <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
  70           </a>
  71           <!--
  72           <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
  73             <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
  74           </a>
  75           -->
  76       </span>
  77
  78       The <a href="library.shtml">knowledge base</a> can be
  79       <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
  80       (locally or on the World Wide Web) and
  81       <a href="http://helm.cs.unibo.it/whelp/"> searched by means of
  82       content-based queries</a>; </p>
  83
  84       <p class="spaced">
  85         <span class="screenshots">
  86           <a class="quiet" href="images/screenshot-tinycals.png">
  87             <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
  88           </a>
  89         </span>
  90         The tactical language, part of the proof language, has
  91         step-by-step semantics, enabling inspection and replaying of deeply
  92         structured proof scripts. </p>
  93
  94       <p>Matita is partially supported by the following Projects: </p>
  95       <ul>
  96         <li><a href="http://www.cs.chalmers.se/Cs/Research/Logic/Types/">
  97           Types Project</a></li>
  98        <li><a href="http://www.mctafi.math.unipd.it/">McTafi</a></li>
  99        <li><a href="http://dama.cs.unibo.it/">Dama</a></li>
 100       </ul>
 101
 102       <!--#include virtual="bottombar.shtml" -->
 103     </div>
 104   </body>
 105 </html>