Matita e' un tool sperimentale di supporto alla dimostrazione interattiva di teoremi e alla verifica di correttezza del software, 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. L'applicazione adotta una filosofia di scrittura delle prove basata su tattiche, cioe' comandi impartiti dall'utente al sistema che lo indirizzano verso la ricostruzione della dimostrazione. Lambda-termini di prova (codificati in XML) sono prodotti per la memorizzazione di lungo periodo e lo scambio di dati con altri sistemi. 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 semantiche. Ulteriori informazioni possono essere ottenute alla home-page dell'applicazione, all'indirizzo http://matita.cs.unibo.it/matita
A.Asperti, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli (2007). Matita.
Matita
ASPERTI, ANDREA;SACERDOTI COEN, CLAUDIO;TASSI, ENRICO;
2007
Abstract
Matita e' un tool sperimentale di supporto alla dimostrazione interattiva di teoremi e alla verifica di correttezza del software, 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. L'applicazione adotta una filosofia di scrittura delle prove basata su tattiche, cioe' comandi impartiti dall'utente al sistema che lo indirizzano verso la ricostruzione della dimostrazione. Lambda-termini di prova (codificati in XML) sono prodotti per la memorizzazione di lungo periodo e lo scambio di dati con altri sistemi. 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 semantiche. Ulteriori informazioni possono essere ottenute alla home-page dell'applicazione, all'indirizzo http://matita.cs.unibo.it/matitaI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
