The Mizar System is the only implementation of the Mizar Language. Originally, the Mizar system was implemented on an IBM-PC x86 compatibles under MS DOS. Now we distribute releases for MS Windows and Intel-based Linux and Solaris. The whole Mizar system (including verifier) is coded in Pascal using the Free Pascal compiler.
Andrzej Trybulec is the author of the Mizar Language, he is also the head of the team implementing the verifier:
The mechanics of preparing a Mizar Article is as follows:
mizf (or mizf.bat) user script.
Alternatively, Josef Urban's
Emacs-lisp Mizar mode
(now included in all Mizar distributions)
provides a fully functional interface to the Mizar System.
When finished, an article is submitted to the Library Committee of Association of Mizar Users for inclusion into the Mizar Mathematical Library. The contributed article is subject to a review and if needed the authors must revise their file. The contents of an accepted article is extracted by the Exporter utility and incorporated into the public data base distributed to all Mizar users.
The distribution of the Mizar system and the Mizar Mathematical Library is free of charge for non commercial purposes.
NOTE: Mizar is not exactly free software. Almost all material is copyrighted.
The authors would like to keep track who is using the system. If you are using Mizar for whatever purpose, please report it toRoman Matuszewski (Mizar Users Group) romat@mizar.orgor print the file decl.txt, fill in and send signed the Mizar User Declaration, toMizar Users Group
Lasek Brzozowy 15/9
02-792 Warsaw
POLAND
Last modified: December 6, 2003