<!--#include virtual="xhtml-header.shtml" -->
<html>
<head>
+ <meta name="keywords" content="Matita, prover, assistant" />
<title>Matita - Home Page</title>
<!--#include virtual="xhtml-meta.shtml" -->
</head>
<div class="main">
<div class="topimage">
- <img src="images/matita-text-big.png" alt="Big Matita label" />
+ <img src="images/matita-text-big.png" alt="Matita" />
+ <a href="matita_it.shtml">
+ <img src="flags/wit.gif" alt="italian flag" />
+ </a>
</div>
<p class="spaced">
-->
</span>
- The knowledge base can be
+ 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
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:
+ <ul>
+ <li><a href=http://www.cs.chalmers.se/Cs/Research/Logic/Types/>
+ Types Project</a>
+ <li><a href=http://www.mctafi.math.unipd.it/>McTafi</a></li>
+ </ul>
+ </p>
<!--#include virtual="bottombar.shtml" -->
</div>
--- /dev/null
+<!-- $Id: matita.shtml 6610 2006-07-14 12:06:30Z zacchiro $ -->
+<!--#include virtual="xhtml-header.shtml" -->
+<html>
+ <head>
+ <meta name="keywords" content="Matita, prover, assistant" />
+ <title>Matita - Home Page Italiana</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+ </head>
+ <body>
+ <!--#include virtual="menubar_it.shtml" -->
+ <!--#include virtual="news_it.shtml" -->
+ <div class="main">
+
+ <div class="topimage">
+ <img src="images/matita-text-big.png" alt="Matita" />
+ <a href="matita.shtml">
+ <img src="flags/wgb.gif" alt="english flag" />
+ </a>
+ </div>
+
+ <p class="spaced">
+ Matita e' un tool sperimentale di supporto alla dimostrazione
+ interattiva di teoremi, in via di sviluppo al
+ <a href="http://www.cs.unibo.it">Dipartimento di Scienze
+ dell'Informazione</a> della
+ <a href="http://www.unibo.it">Universita' degli Studi di Bologna</a>.
+ </p>
+
+<!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
+
+ <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 e' basato sul Calcolo delle Costruzioni (Co)Induttive, ed
+ parzialmente compatibile con l'analogo strumento francese
+ <a href="http://coq.inria.fr">Coq</a>.
+ Matita e' una applicazione ragionevolmente semplice e piccola,
+ la cui complessita' architetturale puo' essere
+ padroneggiata da laureandi, facendone uno strumento particolarmente
+ utile per la sperimentazione di nuove idee e soluzioni in ambito
+ universitario.
+ Matita adotta una filosofia di scrittura delle prove basata su
+ tattiche; lambda-termini di prova (codificati in XML) sono prodotti
+ per la memorizzazione di lungo periodo e lo scambio di dati
+ con altri sistemi.
+ </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>
+ L'interfaccia grafica e' stata ispirata da CtCoq e
+ <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
+ Supporta una resa bidimensionale di alta qualita' delle espressioni
+ basata sul markup
+ <a href="http://www.w3.org/Math/">MathML</a>.</p>
+
+ <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>
+
+ La <a href="library.shtml">base di conoscenza matematica</a> puo'
+ essere
+ <a href="http://helm.cs.unibo.it/browse/">visitata</a> come un ipertesto
+ (localmente o sul World Wide Web) e si possono effettuare
+ <a href="http://helm.cs.unibo.it/whelp/">ricerche</a> basate su
+ interrogazioni contenutistiche; </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>
+ Il linguaggio delle tattiche, parte del vernacolo di prova,
+ ha una semantica passo-passo che consente di ispezionare e
+ eseguire in modo non atomico anche scripts altamente strutturati.</p>
+
+ <p>Matita e' finanziato parzialmente dai seguenti progetti:
+ <ul>
+ <li><a href=http://www.cs.chalmers.se/Cs/Research/Logic/Types/>
+ Types Project</a>
+ <li><a href=http://www.mctafi.math.unipd.it/>McTafi</a></li>
+ </ul>
+ </p>
+ <!--#include virtual="bottombar.shtml" -->
+ </div>
+ </body>
+</html>
projects / helm.git / commitdiff