</head>
<body>
<!--#include virtual="menubar.shtml" -->
+ <!--#include virtual="news.shtml" -->
<div class="main">
<div class="topimage">
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
+ <p>
+ <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 <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
+ 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 class="with_screenshots">
+ <ul>
<li>
<p>