<!--#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>
<body>
<!--#include virtual="menubar.shtml" -->
+ <!--#include virtual="news.shtml" -->
<div class="main">
- <div class="topimage">
- <img src="images/matita-text-big.png" />
- </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> Matita is <strong>traditional</strong>. Its logical foundation is the
- Calculus of (Co)Inductive Constructions (CIC), and it can re-use
- mathematical concepts produced by other proof assistants like
- <a href="http://coq.inria.fr">Coq</a> and encoded in an
- <a href="http://www.w3.org/XML/">XML</a> dialect. The interaction
- paradigm of Matita is well known, having been inspired by
- <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>, and its
- proof language is procedural in the same spirit of LCF. </p>
-
- <p> Matita is <strong>innovative</strong>: </p>
- <ul class="wide">
+ <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>
- <li> its user interface sports high quality bidimensional rendering of
- proofs and formulae exploiting
- <a href="http://www.w3.org/Math/">MathML</a> markup, equipped with
- direct manipulation of the underlying CIC terms; </li>
+<!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
- <li> its library is distributed: every authored concepts can be
- published and become part of the Matita library which can be browsed as
- an hypertext (locally or on the World Wide Web) and searched by means of
- content-based queries; </li>
- <li> the tactical language, part of the proof language, has
- step-by-step semantics, enabling inspection and replaying of deeply
- structured proof scripts </li>
-
- </ul>
-
- <!--#include virtual="bottombar.shtml" -->
</div>
</body>
</html>
-<!-- $Id$ -->
projects / helm.git / blobdiff