Copenhagen Programming Language Seminar

The Mizar System

Artur Kornilowicz
University of Bialystok, Poland

Thursday, May 31, 13:15-16:00 (!)
DIKU, Universitetsparken 1, Room N026/S125


Mizar is a proof checker suitable for formal verification of mathematical proofs, where proofs are based on Jaskowski natural deduction. Mizar is also a language in which these texts are written. The language is intended to be understandable both by computers and humans. The huge part of the system is the Mizar Mathematical Library, a collection of Mizar articles containing proofs of mathematical facts.

We present:

  • basic parts of Mizar syntax;
  • some tactics of proofs allowed by Mizar;
  • ways of making reasonings shorter using advanced Mizar features;
  • most valuable facts verified by Mizar.
At the end we present some directions in which Mizar development goes to straighten the power of the verifier.

The first hour is the COPLAS talk proper. Afterwards, there will be an opportunity for interested attendees to try out the system themselves.

Scientific host: Klaus Grue. Administrative host: Camilla Torp-Smith. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org