Next: Birmingham
Up: Cooperating sites
Previous: Bergen


The Mizar Group (now at the University in Bialystok - UWB) led by Andrzej Trybulec has been developing a proof checker system for almost three decades. The input language of the system, called Mizar, is close to informal mathematical language and enjoys rich linguistic structure: open vocabularies, flexible syntax, dependent types (allowing for overloading and hidden arguments), adjectives and structures (record types) with inheritance. The system is based on classical logic - Fitch-Jaskowski system of conditional proofs.

The main activities of the project are:

UWB cooperates with KUN (Nijmegen). The cooperation includes parallel development, e.g. the formalization of a proof of FTA done almost simultaneously with some theoretical work. We continue long term and fruitful exchange of the ideas with U. of Durham (mathematical vernacular, subtyping) and other groups.

In this proposal, the group will mainly address the objective of Formal Mathematics, focussing on mathematical vernacular language and the use of ideas from type theory, such as coercive subtyping or generic metastructures (modules in Coq or locale in Isabelle), in classical mathematics.

The senior members of the Mizar Group are

Bialystok homepage

Bengt Nordström 2005-09-22