]> matita.cs.unibo.it Git - helm.git/blob - helm/www/matita/matita.shtml
add comment
[helm.git] / 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>