À propos de cet article
Publié en ligne: 05 janv. 2011
Pages: 65 - 75
DOI: https://doi.org/10.2478/v10037-010-0009-7
This content is open access.
The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from [6] and [7]. 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 the unification of Mizar expressions.