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: