Matita Development

Matita Developers

The origins of Matita go back to 1999 and are intertwined with the HELM Project. Since then, a diff --git a/helm/www/matita/download.shtml b/helm/www/matita/download.shtml index 1588aeb79..1c07e00b2 100644 --- a/helm/www/matita/download.shtml +++ b/helm/www/matita/download.shtml @@ -11,13 +11,17 @@

Download Matita!

Releases

Matita has no official releases yet. +

License

All our source code is released under the terms of the GNU General Public Licence and is publically accessible on our Subversion repository. +

Subversion repository

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index 33a658479..4a53073af 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -2,6 +2,7 @@ + Matita - Home Page @@ -11,7 +12,10 @@

+ +

@@ -71,7 +75,7 @@ --> - The knowledge base can be + The knowledge base can be browsed as an hypertext (locally or on the World Wide Web) and searched by means of @@ -86,6 +90,14 @@ The tactical language, part of the proof language, has step-by-step semantics, enabling inspection and replaying of deeply structured proof scripts.

+ +

Matita is partially supported by the following Projects: +

+ Types Project +
McTafi

diff --git a/helm/www/matita/matita_it.shtml b/helm/www/matita/matita_it.shtml new file mode 100644 index 000000000..379be3d53 --- /dev/null +++ b/helm/www/matita/matita_it.shtml @@ -0,0 +1,109 @@ + + + + + + Matita - Home Page Italiana + + + + + +

+ +

+ Matita e' un tool sperimentale di supporto alla dimostrazione + interattiva di teoremi, in via di sviluppo al + Dipartimento di Scienze + dell'Informazione della + Universita' degli Studi di Bologna. +

+ + + +

+ + + + + + + Matita e' basato sul Calcolo delle Costruzioni (Co)Induttive, ed + parzialmente compatibile con l'analogo strumento francese + Coq. + 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. +

+ +

+ + + + + + + + + L'interfaccia grafica e' stata ispirata da CtCoq e + Proof General. + Supporta una resa bidimensionale di alta qualita' delle espressioni + basata sul markup + MathML.

+ +

+ + + + + + + + + + + La base di conoscenza matematica puo' + essere + visitata come un ipertesto + (localmente o sul World Wide Web) e si possono effettuare + ricerche basate su + interrogazioni contenutistiche;

+ +

+ + + + + + 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.

+ +

Matita e' finanziato parzialmente dai seguenti progetti: +

+ Types Project +
McTafi

+ +

+ + diff --git a/helm/www/matita/menubar.shtml b/helm/www/matita/menubar.shtml index 2178235c9..3c06e1836 100644 --- a/helm/www/matita/menubar.shtml +++ b/helm/www/matita/menubar.shtml @@ -7,7 +7,13 @@

diff --git a/helm/www/matita/news.shtml b/helm/www/matita/news.shtml index e478812f7..eeab8cfac 100644 --- a/helm/www/matita/news.shtml +++ b/helm/www/matita/news.shtml @@ -3,6 +3,13 @@

News:

21 Aug 2006
+ Matita-prover on TPTP. +
18 Jul 2006
+ the scripts of the library are now + on-line +
14 Jun 2006
mailing lists for Matita are now available diff --git a/helm/www/matita/style.css b/helm/www/matita/style.css index d129be452..a53015662 100644 --- a/helm/www/matita/style.css +++ b/helm/www/matita/style.css @@ -28,9 +28,9 @@ div.news { top: 25px; left: 845px; font-size: 10pt; - width: 100px; + width: 105px; background: #eaeaea; - padding: 10px; + padding: 5px; } /* site-wide typesetting */ @@ -106,7 +106,12 @@ div.menu ul li { } div.menu ul li a { + display: block; + text-align: right; text-decoration: none; + vertical-align: middle; + height: 45px; + background-repeat: no-repeat; } a.menu:hover { -- 2.39.5