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

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/matita
A.Asperti; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/47115
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact