- <dl id="matitaMap">
- <dt id="developers">1. Developers</dt>
- <dd id="developersDef"><a href="developers.shtml"></a></dd>
- <dt id="documentation">2. Documentation</dt>
- <dd id="documentationDef"><a href="documentation.shtml"></a></dd>
- <dt id="community">3. Community</dt>
- <dd id="communityDef"><a href="community.shtml"></a></dd>
- <dt id="download">4. Download</dt>
- <dd id="downloadDef"><a href="download.shtml"></a></dd>
- </dl>
- <div>
-
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
+ <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
+ </a>
+ <a class="quiet" href="images/screenshot-cicbrowser-query.png">
+ <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
+ </a>
+ <!--
+ <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
+ <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
+ </a>
+ -->
+ </span>
+
+ The <a href="library.shtml">knowledge base</a> can be
+ <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
+ (locally or on the World Wide Web) and
+ <a href="http://helm.cs.unibo.it/whelp/"> searched by means of
+ content-based queries</a>; </p>
+
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-tinycals.png">
+ <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
+ </a>
+ </span>
+ The tactical language, part of the proof language, has
+ step-by-step semantics, enabling inspection and replaying of deeply
+ structured proof scripts. </p>
+
+ <p>Matita is partially supported by the following Projects: </p>
+ <ul>
+ <li><a href="http://www.cs.chalmers.se/Cs/Research/Logic/Types/">
+ Types Project</a></li>
+ <li><a href="http://www.mctafi.math.unipd.it/">McTafi</a></li>
+ <li><a href="http://dama.cs.unibo.it/">Dama</a></li>
+ </ul>
+
+ <!--#include virtual="bottombar.shtml" -->
+ </div>