Mizar, is the second magnitude star set in the
middle of the Big Dippper's handle; Mizar is a quadruple star.
The Mizar project is a long-term effort aimed at developing software
to support a working mathematician in preparing papers.
A. Trybulec, the leader of the project,
has designed a language for writing formal mathematics.
The logical structure of the language is based on a natural
deduction system developed by Jaskowski.
The texts written in the language are called Mizar articles and are organized
into a data base.
The Tarski-Grothendieck set theory forms the basis of doing mathematics in
The implemented processor of the language checks the articles for logical
consistency and correctness of references to other articles.
Why do I bother with all
this? Even more reasons: a presentation at the NA MKM 2004 in Phoenix (pdf) .
Mizar Verification of Algorithms for Recognizing Chordal Graphs,
Broderick Arneson, MSc Thesis, January 2007,
The first 30 years, by R. Matuszewski and P. Rudnicki, presented
at a MKM 2004 workshop, appeared in Mechanized Mathematics and its
Applications, Vol. 4, No. 1, March 2005, pp. 3-24 (preliminary versions:
Verification of graph algorithms in Mizar, Glibert Lee,
MSc thesis, 2004, (.ps).
A report on the progress of the CCL project by
G. Bancerek and P. Rudnicki, submitted to Journal of Authomated
Reasoning in May 2002, .ps. A
shortened version appeared in JAR, V 29, No 3-4, pp 189-224, 2002.
A paper for Calculemus 2000, appeared as
Rudnicki, P. and Schwarzweller, C. and Trybulec, A.,
Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000
Symposium , Eds. Kerber, M. and Kohlhase, M. A K Peters, pp. 191--204.
An extended version of the above
appeared as Rudnicki, P. and Schwarzweller, C. and Trybulec, A.,
Commutative Algebra in the Mizar System, Journal of Symbolic Computation,
2001, 32, pp. 143--169.
A Collection of TeXed Mizar Abstracts
(postscript, 1MB), originally Technical Report TR 89-19,
Dept. of CS, U of Alberta. This was the humble beginning of typestting
Mizar abstracts in TeX which led to Formalized Mathematics.