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 class="spaced">
  18       Matita (that means <em>pencil</em> in italian) is an experimental,
  19         interactive theorem prover under development at the
  20       <a href="http://www.cs.unibo.it">Computer Science Department</a> of the
  21       <a href="http://www.unibo.it">University of Bologna</a>.
  22       </p>
  23
  24 <!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
  25
  26       <p class="spaced">
  27       <span class="screenshots">
  28         <a class="quiet" href="images/screenshot-matita.png">
  29           <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
  30         </a>
  31       </span>
  32
  33       Matita is based on the
  34       Calculus of (Co)Inductive Constructions, and is compatible, at some
  35       extent, with <a href="http://coq.inria.fr">Coq</a>.
  36       It is a reasonably small and simple application, whose
  37       architectural and software complexity is meant to be mastered by
  38       students, providing a tool particularly suited for testing innovative
  39       ideas and solutions.
  40       Matita adopts a tactic based editing mode; (XML-encoded) proof objects
  41       are produced for storage and exchange.
  42       </p>
  43
  44       <p class="spaced">
  45       <span class="screenshots">
  46           <a class="quiet" href="images/screenshot-matita-href.png">
  47             <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
  48           </a>
  49           <a class="quiet" href="images/screenshot-matita-selection.png">
  50             <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
  51           </a>
  52         </span>
  53       The graphical interface has been inspired by CtCoq and
  54       <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
  55       It supports high quality bidimensional rendering of
  56       proofs and formulae transformed on-the-fly to
  57       <a href="http://www.w3.org/Math/">MathML</a> markup</p>
  58
  59       <p class="spaced">
  60       <span class="screenshots">
  61           <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
  62             <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
  63           </a>
  64           <a class="quiet" href="images/screenshot-cicbrowser-query.png">
  65             <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
  66           </a>
  67           <!--
  68           <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
  69             <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
  70           </a>
  71           -->
  72       </span>
  73
  74       The knowledge base can be
  75       <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
  76       (locally or on the World Wide Web) and
  77       <a href="http://helm.cs.unibo.it/whelp/"> searched by means of
  78       content-based queries</a>; </p>
  79
  80       <p class="spaced">
  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
  90       <!--#include virtual="bottombar.shtml" -->
  91     </div>
  92   </body>
  93 </html>