<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml">The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from [14] and [13]. The theory here presented is an abstract of the existing implementation of the Mizar system and is devoted to the formalization of Mizar expressions. The base idea behind the formalization is dependence on variables which is determined by variable-dependence (variables may depend on other variables). The dependence constitutes a Galois connection between opposite poset of dependence-closed set of variables and the sup-semilattice of widening of Mizar types (smooth type widening).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 <italic>quasi</italic> 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 result, there is no possibility to conduct 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 <italic>identification</italic> 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 structures and algorithms from the Mizar checker (like <italic>equational classes</italic>).MML identifier: ABCMIZ 1, version: 7.9.01 4.101.1015</abstract>

The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from [14] and [13]. The theory here presented is an abstract of the existing implementation of the Mizar system and is devoted to the formalization of Mizar expressions. The base idea behind the formalization is dependence on variables which is determined by variable-dependence (variables may depend on other variables). The dependence constitutes a Galois connection between opposite poset of dependence-closed set of variables and the sup-semilattice of widening of Mizar types (smooth type widening).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 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 result, there is no possibility to conduct 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 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 structures and algorithms from the Mizar checker (like equational classes).MML identifier: ABCMIZ 1, version: 7.9.01 4.101.1015

Towards the Construction of a Model of Mizar Concepts

Formalized Mathematics

{"article-title":"Towards the Construction of a Model of Mizar Concepts"}

The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from [14] and [13]. The theory here presented is an...

Towards the Construction of a Model of Mizar Concepts

Publicado en línea: 20 mar 2009

Páginas: 207 - 230

DOI: https://doi.org/10.2478/v10037-008-0027-x

This content is open access.