Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 The Mizar Project
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
Mizar.
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) .
A report on the progress of the
CCL project by G. Bancerek and P. Rudnicki, submitted to
Journal of Authomated Reasoning in May 2002. As it is quite
long probably only a part of it, if any, will appear in print.
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 general introduction to Mizar is in
On Equivalents of Well-foundedness
by P. Rudnicki and A. Trybulec, appeared in Journal of Automated
Reasoning, 23: 197-234, 1999.
An outline of PC-Mizar
by M. Muzalewski. Obsolete but still informative sort of a manual.
For a general (now obsolete) overview of the project look into
An Overview of the Mizar project by P. Rudnicki.
The paper was presented in Bastaad, Sweden in June 1992.
A small tutorial
for new users; based on
A report on a Mizar demo
at the Dagstuhl "Deduction" seminar, Feb 27, 1997,
by P. Rudnicki (obsolete as it is for Mizar 5.2.20)
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.