Matita 0.5.7

Matita e' un dimostratore interattivo di teoremi basato su una variante del Calcolo delle Costruzioni CoInduttive. Il software, che e' open source, e' rilasciato ai termini della GNU General Public Licence ed e' pubblicamente accessibile al nostro Subversion repository. Matita e' scritto in OCAML. La dimensione attuale dell'applicazione si aggira sulle 90.000 linee di codice. La versione 0.5.7 implementa e permette di testare qualitativamente e quantitativamente diverse nuove funzionalita' descritte e studiate nei lavori di ricerca degli autori pubblicati nel 2008. In particolare: 1) un innovativo meccanismo di gestione delle coercion che permette di effettuare inferenza di tipi in presenza di ereditarieta' multipla fra strutture matematiche; 2) il supporto per pattern notazionali non lineari, con applicazioni allo sviluppo a livello utente di interfacce didattiche per la rappresentazione di alberi di derivazione anche mal formati; 3) l'implementazione di un nuovo meccanismo di universi algebrici per la stratificazione predicativa di definizioni matematiche;