The Mizar Language. Selected Topics.

Andrzej Trybulec, University of Warsaw, Bialystok Compus, Poland

Abstract:

The design of a language for computer aided practical formalization of mathematics must meet specific requirements on different levels. I will present solutions adopted in the Mizar language for selected problems:
  1. How to cope with an open vocabulary? The concept of the lexical environment of an article.
  2. Why syntactic types are needed ? Hidden arguments of constructors.
  3. How to cope with the udefiniteness? Permissiveness.
  4. The role of adjectives in mathematical vernacular.
  5. How to do modern mathematics?. A concept of the structure, close to the structure in the Bourbaki sense.