An Introductory Comment on Mizar MSE
"Of yours" means here:
computer scientists concerned with mechanized theorem proving
Though there is a lot of theorem provers and proof checkers the whole Web over, the software in question is specially appreciated and recommendable. Why?
It is remarkably natural among natural deduction systems as most approximating the English vernacular of mathematical proofs. Furthermore, it is most practical because of the inference rules being so devised that proofs become short and concise; its handy logical symbolism, confined to pure ASCII, makes it as universal as was Latin in the old good times.
Mizar MSE is a proof-checker to assist humans in their strive for
logical correctness.
"MSE" stands for Multi-Sorted [first order logic
with] Equality, while MIZAR is the star to luckily shine over
the project.
Mizar MSE is just a very small subset of full Mizar as developed by the team established by the Mizar's author Andrzej Trybulec (Warsaw University, Bialystok Branch, PL). The latter is associated with the QED Project. See mentions on Mizar by Harrison and Kerber. The big Mizar system involves a proof-checker which offers a wide spectrum of logical means for theorem proving as well as powerful devices for building mathematical knowledge representations in a data base form. On the other hand, the "small" Mizar (called "baby Mizar" by its author) is restricted to `raw' predicate calculus, it even does not include functional notation. Nevertheless, it offers fine services in the areas listed at the beginning.
This issue is devoted to the use of Mizar MSE in teaching basic logic and pieces of elementary mathematics; it contains also a discussion of Mizar's historical connexions with mathematical practice, as patterned on Euclid, and with the Polish stream of natural deduction (S. Jaskowski, etc). The former is dealt with by Hoover and Rudnicki, a report concerned with teaching prospective computer scientists, and in the concise textbook by M. Mostowski (which is worth presenting for its general introductory ideas). The latter approach is represented by Witold Marciszewski's contribution.