Sistema Mizar
Il sistema Mizar costituisce l'oggetto principale del progetto Mizar. Consiste di un linguaggio per la scrittura formalizzata di definizione e dimostrazioni matematiche, un programma per computer capace di verificare dimostrazioni scritte in questo linguaggio e una libreria di definizioni e teoremi già dimostrati.
Il progetto Mizar ha preso vita nel 1973. È portato avanti da Andrzej Trybulec (fondatore) e dalle università di Białystok (Polonia), Alberta (Canada) e Shinshu (Giappone). I suoi obiettivi sono simili a quelli del Progetto QED, proposto da Bob Boyer nel 1993.
Il sistema modifica
La Mizar Mathematical Library (MML) è costruita sul sistema di assiomi Tarski-Grothendieck. A marzo 2008 conteneva circa 8.800 definizioni e 46.000 teoremi[1]. Nuovi articoli sono esaminati dalla Commissione degli Utenti e pubblicati nell'associato Journal of Formalized Mathematics[2].
Il linguaggio è assai simile al linguaggio matematico convenzionale. È possibile definire e utilizzare costrutti sintattici in luogo dei simboli. Gli articoli sono scritti in ASCII e sono lunghi dalle 1.500 alle 5.000 parole.
Il programma per verificare le dimostrazioni è scritto in Pascal, è disponibile per i più diffusi sistemi operativi e può essere scaricato gratuitamente per scopi non commerciali. Il codice sorgente è accessibile solo agli utenti registrati.[3]
Note modifica
- ^ see [1] for up-to-date statistics
- ^ Journal of Formalized Mathematics
- ^ Association of Mizar Users
Voci correlate modifica
Collegamenti esterni modifica
- Main Mizar site, contiene link alla MML, al Journal of Formalized Mathematics e una bibliografia.
- MML Query, is a search engine for MML.
- Freek Wiedijk's Mizar site, contains slides of a conference talk about the system, as well as a 40 page introductory article
- Association of Mizar Users, su mizar.uwb.edu.pl.
- A paper about Mizar history( Archiviato l'11 ottobre 2008 in Internet Archive.)
- Mizar wiki [collegamento interrotto], su wiki.mizar.org.