+ <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> Matita is <strong>innovative</strong>: </p>
+ <ul class="wide">
+
+ <li> 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; </li>
+
+ <li> the knowledge base is distributed: every authored concepts can be
+ published becoming 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>