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.

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]

• Progetto QED
• Automath

• 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.