-<!-- $Id$ -->
<!--#include virtual="xhtml-header.shtml" -->
-<html>
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
<head>
+ <meta name="keywords" content="Matita, prover, assistant" />
<title>Matita - Home Page</title>
<!--#include virtual="xhtml-meta.shtml" -->
</head>
<div class="main">
<div class="topimage">
- <img src="images/matita-text-big.png" alt="Big Matita label" />
+ <img src="images/matita-text-big.png" alt="Matita" />
+ <a href="matita_it.shtml">
+ <img src="flags/wit.gif" alt="italian flag" />
+ </a>
</div>
- <p> Matita is a new document-centric interactive theorem prover that
- integrates several <a href="http://www.mkm-ig.org">Mathematical Knowledge
- Management</a> tools and techniques. </p>
+ <p class="spaced">
+ Matita (that means <em>pencil</em> in italian) is an experimental,
+ interactive theorem prover under development at the
+ <a href="http://www.cs.unibo.it">Computer Science Department</a> of the
+ <a href="http://www.unibo.it">University of Bologna</a>.
+ </p>
- <p>
+<!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
+
+ <p class="spaced">
<span class="screenshots">
<a class="quiet" href="images/screenshot-matita.png">
<img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
</a>
</span>
- Matita is <strong>traditional</strong>. Its logical foundation is the
- Calculus of (Co)Inductive Constructions (CIC). It can re-use
- mathematical concepts produced by other proof assistants (e.g.
- <a href="http://coq.inria.fr">Coq</a>) when encoded in an
- <a href="http://www.w3.org/XML/">XML</a> representation of CIC. The
- interaction paradigm of Matita is familiar, being inspired by CtCoq and
- <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>. Its
- proof language is procedural in the same spirit of LCF. </p>
-
- <p> Matita is <strong>innovative</strong>: </p>
- <ul>
-
- <li>
- <p>
- <span class="screenshots">
+
+ Matita is based on the
+ Calculus of (Co)Inductive Constructions, and is compatible, at some
+ extent, with <a href="http://coq.inria.fr">Coq</a>.
+ It is a reasonably small and simple application, whose
+ architectural and software complexity is meant to be mastered by
+ students, providing a tool particularly suited for testing innovative
+ ideas and solutions.
+ Matita adopts a tactic based editing mode; (XML-encoded) proof objects
+ are produced for storage and exchange.
+ </p>
+
+ <p class="spaced">
+ <span class="screenshots">
<a class="quiet" href="images/screenshot-matita-href.png">
<img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
</a>
<img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
</a>
</span>
- the user interface sports high quality bidimensional rendering of
- proofs and formulae transformed on-the-fly to <a
- href="http://www.w3.org/Math/">MathML</a> markup, on which direct
- manipulation of the underlying CIC terms is still possible;
- </p>
- </li>
+ The graphical interface has been inspired by CtCoq and
+ <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
+ It supports high quality bidimensional rendering of
+ proofs and formulae transformed on-the-fly to
+ <a href="http://www.w3.org/Math/">MathML</a> markup</p>
- <li>
- <p>
- <span class="screenshots">
+ <p class="spaced">
+ <span class="screenshots">
<a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
<img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
</a>
</a>
<!--
<a class="quiet" href="images/screenshot-cicbrowser-proof.png">
- <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering" />
+ <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
</a>
-->
- </span>
- the knowledge base is distributed: every authored concepts can be
- published becoming part of the Matita library which can be <a
- href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
- (locally or on the World Wide Web) and <a
- href="http://helm.cs.unibo.it/whelp/"> searched by means of
- content-based queries</a>; </p>
- </li>
+ </span>
+
+ The <a href="library.shtml">knowledge base</a> can be
+ <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
+ (locally or on the World Wide Web) and
+ <a href="http://helm.cs.unibo.it/whelp/"> searched by means of
+ content-based queries</a>; </p>
- <li>
- <p>
+ <p class="spaced">
<span class="screenshots">
<a class="quiet" href="images/screenshot-tinycals.png">
<img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
</a>
</span>
- the tactical language, part of the proof language, has
+ The tactical language, part of the proof language, has
step-by-step semantics, enabling inspection and replaying of deeply
structured proof scripts. </p>
- </li>
-
+
+ <p>Matita is partially supported by the following Projects: </p>
+ <ul>
+ <li><a href="http://www.cs.chalmers.se/Cs/Research/Logic/Types/">
+ Types Project</a></li>
+ <li><a href="http://www.mctafi.math.unipd.it/">McTafi</a></li>
+ <li><a href="http://dama.cs.unibo.it/">Dama</a></li>
</ul>
<!--#include virtual="bottombar.shtml" -->
projects / helm.git / blobdiff