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

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]