- 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">