@misc{ABCMIZ_1.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {Towards the construction of a model of Mizar concepts},
  SECTION1  = {Variables},
  SECTION2  = {Quasi-loci},
  SECTION3  = {Mizar Constructor Signature},
  SECTION4  = {Mizar Expressions},
  SECTION5  = {Quasi-terms},
  SECTION6  = {Quasi-adjectives},
  SECTION7  = {Quasi-types},
  SECTION8  = {Variables in Quasi-types},
  SECTION9  = {Smooth Type Widening},
  SECTION10 = {Structural Induction},
  SECTION11 = {Substitution},
  DAY = {21},
  MONTH = {April},
  YEAR = {2008},
  ADDRESS1 = {Bia{\l}ystok Technical University},
  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_0.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 base idea behind the
  formalization is dependence from variables which is determined by
  variable-dependence (variables may depend from another variables).
  The dependence stands a Galois connection between opposite poset of
  dependence-closed set of variables and the sup-semilattice of widening
  of Mizar types (smooth type widening).\par
  In the paper the concepts strictly connected with Mizar expressions
  are formalized.  Among them are quasi-loci, quasi-terms,
  quasi-adjectives, and quasi-types.  The structural induction and
  operation of substitution are, also, introduced. The prefix {\it
  quasi} is used to indicate that some rules of construction of Mizar
  expressions may not be fulfilled. For example, variables, quasi-loci,
  and quasi-terms have no assigned types and, in the result, there is no
  possibility to do type-checking of arguments. The other gaps concern
  inconsistent and out-of-context clusters of adjectives in types. Those
  rules are required in the Mizar {\it identification} process. However,
  the expression appearing in later processes of Mizar checker may not
  satisfy the rules. So, introduced apparatus is enough and adequate to
  describe data structuers and algorithms from Mizar checker (like {\it
  equational classes}).}}
