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" />
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>.
24 <!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
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" />
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
40 Matita adopts a tactic based editing mode; (XML-encoded) proof objects
41 are produced for storage and exchange.
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" />
49 <a class="quiet" href="images/screenshot-matita-selection.png">
50 <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
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>
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" />
64 <a class="quiet" href="images/screenshot-cicbrowser-query.png">
65 <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
68 <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
69 <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
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>
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>
90 <!--#include virtual="bottombar.shtml" -->