- <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>
+ <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 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>
+ <a class="quiet" href="images/screenshot-matita-selection.png">
+ <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
+ </a>
+ </span>
+ 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>