+<!-- $Id$ -->
<!--#include virtual="xhtml-header.shtml" -->
<html>
<head>
</head>
<body>
<!--#include virtual="menubar.shtml" -->
+ <!--#include virtual="news.shtml" -->
<div class="main">
<div class="topimage">
- <img src="images/matita-text-big.png" />
+ <img src="images/matita-text-big.png" alt="Big Matita label" />
</div>
<p> Matita is a new document-centric interactive theorem prover that
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
- Calculus of (Co)Inductive Constructions (CIC), and 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> dialect. The interaction
- paradigm of Matita is well known, having been inspired by
- <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>, and its
+ <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 (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="wide">
+ <ul>
- <li> its user interface sports high quality bidimensional rendering of
- proofs and formulae exploiting
- <a href="http://www.w3.org/Math/">MathML</a> markup, equipped with
- direct manipulation of the underlying CIC terms; </li>
+ <li>
+ <p>
+ <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 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;
+ </p>
+ </li>
- <li> its library is distributed: every authored concepts can be
- published and become 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>
+ <p>
+ <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 knowledge base is distributed: every authored concepts can be
+ published becoming part of the Matita library which 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>
+ </li>
- <li> the tactical language, part of the proof language, has
+ <li>
+ <p>
+ <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 </li>
+ structured proof scripts. </p>
+ </li>
</ul>
</div>
</body>
</html>
-<!-- $Id$ -->
projects / helm.git / blobdiff