Mizar, a not very well known proof tool

Freek Wiedijk

ABSTRACT

The Mizar system from Poland is mentioned often, but not many people know it from first hand experience. It is special in the sense that it uses declarative proofs, in contrast to the procedural proofs of most other proof tools. A short overview of the history proof checking will be followed by an introduction to the Mizar system, and an assessment of its strengths and weaknesses.