2 <!--#include virtual="xhtml-header.shtml" -->
5 <title>Matita - Home Page</title>
6 <!--#include virtual="xhtml-meta.shtml" -->
9 <!--#include virtual="menubar.shtml" -->
10 <!--#include virtual="news.shtml" -->
13 <div class="topimage">
14 <img src="images/matita-text-big.png" alt="Big Matita label" />
17 <p> Matita is a new document-centric interactive theorem prover that
18 integrates several <a href="http://www.mkm-ig.org">Mathematical Knowledge
19 Management</a> tools and techniques. </p>
22 <span class="screenshots">
23 <a class="quiet" href="images/screenshot-matita.png">
24 <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
27 Matita is <strong>traditional</strong>. Its logical foundation is the
28 Calculus of (Co)Inductive Constructions (CIC). It can re-use
29 mathematical concepts produced by other proof assistants (e.g.
30 <a href="http://coq.inria.fr">Coq</a>) when encoded in an
31 <a href="http://www.w3.org/XML/">XML</a> representation of CIC. The
32 interaction paradigm of Matita is familiar, being inspired by CtCoq and
33 <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>. Its
34 proof language is procedural in the same spirit of LCF. </p>
36 <p> Matita is <strong>innovative</strong>: </p>
41 <span class="screenshots">
42 <a class="quiet" href="images/screenshot-matita-href.png">
43 <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
45 <a class="quiet" href="images/screenshot-matita-selection.png">
46 <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
49 the user interface sports high quality bidimensional rendering of
50 proofs and formulae transformed on-the-fly to <a
51 href="http://www.w3.org/Math/">MathML</a> markup, on which direct
52 manipulation of the underlying CIC terms is still possible;
58 <span class="screenshots">
59 <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
60 <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
62 <a class="quiet" href="images/screenshot-cicbrowser-query.png">
63 <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
66 <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
67 <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering" />
71 the knowledge base is distributed: every authored concepts can be
72 published becoming part of the Matita library which can be <a
73 href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
74 (locally or on the World Wide Web) and <a
75 href="http://helm.cs.unibo.it/whelp/"> searched by means of
76 content-based queries</a>; </p>
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" />
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>
93 <!--#include virtual="bottombar.shtml" -->