- <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). 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> encoding 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 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>