@misc{ABCMIZ_A.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {A Model of Mizar Concepts -- Unification},
  NOTE1 = {Partially supported by BTU Grant W/WI/1/06
  and UF\&M(B) Teaching Support},
  DAY = {20},
  MONTH = {November},
  YEAR = {2009},
  SECTION1 = {Preliminary},
  SECTION2 = {Standardized Constructor Signature},
  SECTION3 = {Expressions},
  SECTION4 = {Arity},
  SECTION5 = {Unification},
  SECTION6 = {Type Distribution},
  ADDRESS1 = {Bia{\l}ystok Technical University\\
    The University of Finance and Management, Bia{\l}ystok--E{\l}k},
  SUMMARY = {The aim of this paper is to develop a formal theory of Mizar
  linguistic concepts following the ideas from \cite{Bancerek:2003} and
  \cite{ABCMIZ_1.ABS}. The theory presented is an abstraction from the
  existing implementation of the Mizar system and is devoted to the
  formalization of Mizar expressions.
   The concepts formalized here are: standarized constructor signature,
  arity-rich signatures,
  and unification of Mizar expressions.}}
