###### Congruences and Quotient Algebras of BCI-algebras

## Congruences and Quotient Algebras of BCI-algebras

We have formalized the BCI-algebras closely following the book [7] pp. 16-19 and pp. 58-65. Firstly, the article focuses on the properties of the element and then the definition and properties of congruences and quotient algebras are given. Quotient algebras are the basic tools for exploring the structures of BCI-algebras.

###### Formalizing Two Generalized Approximation Operators

## Summary

Rough sets, developed by Pawlak [15], are important tool to describe situation of incomplete or partially unknown information. In this article we give the formal characterization of two closely related rough approximations, along the lines proposed in a paper by Gomolińska [2]. We continue the formalization of rough sets in Mizar [1] started in [6].

###### Extended Euclidean Algorithm and CRT Algorithm

## Summary

In this article we formalize some number theoretical algorithms, Euclidean Algorithm and Extended Euclidean Algorithm [9]. Besides the a gcd b, Extended Euclidean Algorithm can calculate a pair of two integers (x, y) that holds ax + by = a gcd b. In addition, we formalize an algorithm that can compute a solution of the Chinese remainder theorem by using Extended Euclidean Algorithm. Our aim is to support the implementation of number theoretic tools. Our formalization of those algorithms is based on the source code of the NZMATH, a number theory oriented calculation system developed by Tokyo Metropolitan University [8].

###### On the Lattice of Intervals and Rough Sets

## On the Lattice of Intervals and Rough Sets

Rough sets, developed by Pawlak [6], are an important tool to describe a situation of incomplete or partially unknown information. One of the algebraic models deals with the pair of the upper and the lower approximation. Although usually the tolerance or the equivalence relation is taken into account when considering a rough set, here we rather concentrate on the model with the pair of two definable sets, hence we are close to the notion of an interval set. In this article, the lattices of rough sets and intervals are formalized. This paper, being essentially the continuation of [3], is also a step towards the formalization of the algebraic theory of rough sets, as in [4] or [9].

###### Relational Formal Characterization of Rough Sets

## Summary

The notion of a rough set, developed by Pawlak [10], is an important tool to describe situation of incomplete or partially unknown information. In this article, which is essentially the continuation of [6], we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library). Here we drop the classical equivalence- and tolerance-based models of rough sets [12] trying to formalize some parts of [19] following also [18] in some sense (Propositions 1-8, Corr. 1 and 2; the complete description is available in the Mizar script). Our main problem was that informally, there is a direct correspondence between relations and underlying properties, in our approach however [7], which uses relational structures rather than relations, we had to switch between classical (based on pure set theory) and abstract (using the notion of a structure) parts of the Mizar Mathematical Library. Our next step will be translation of these properties into the pure language of Mizar attributes.

###### Tarski Geometry Axioms

## Summary

This is the translation of the Mizar article containing readable Mizar proofs of some axiomatic geometry theorems formulated by the great Polish mathematician Alfred Tarski [8], and we hope to continue this work.

The article is an extension and upgrading of the source code written by the first author with the help of miz3 tool; his primary goal was to use proof checkers to help teach rigorous axiomatic geometry in high school using Hilbert’s axioms.

This is largely a Mizar port of Julien Narboux’s Coq pseudo-code [6]. We partially prove the theorem of [7] that Tarski’s (extremely weak!) plane geometry axioms imply Hilbert’s axioms. Specifically, we obtain Gupta’s amazing proof which implies Hilbert’s axiom I1 that two points determine a line.

The primary Mizar coding was heavily influenced by [9] on axioms of incidence geometry. The original development was much improved using Mizar adjectives instead of predicates only, and to use this machinery in full extent, we have to construct some models of Tarski geometry. These are listed in the second section, together with appropriate registrations of clusters. Also models of Tarski’s geometry related to real planes were constructed.

###### On Algebras of Algorithms and Specifications over Uninterpreted Data

## Summary

This paper continues formalization in Mizar [2, 1] of basic notions of the composition-nominative approach to program semantics [13] which was started in [8, 11].

The composition-nominative approach studies mathematical models of computer programs and data on various levels of abstraction and generality and provides tools for reasoning about their properties. Besides formalization of semantics of programs, certain elements of the composition-nominative approach were applied to abstract systems in a mathematical systems theory [4, 6, 7, 5, 3].

In the paper we introduce a definition of the notion of a binominative function over a set *D* understood as a partial function which maps elements of *D* to *D*. The sets of binominative functions and nominative predicates [11] over given sets form the carrier of the generalized Glushkov algorithmic algebra [14]. This algebra can be used to formalize algorithms which operate on various data structures (such as multidimensional arrays, lists, etc.) and reason about their properties.

We formalize the operations of this algebra (also called compositions) which are valid over uninterpretated data and which include among others the sequential composition, the prediction composition, the branching composition, the monotone Floyd-Hoare composition, and the cycle composition. The details on formalization of nominative data and the operations of the algorithmic algebra over them are described in [10, 12, 9].

###### Binary Relations-based Rough Sets – an Automated Approach

## Summary

Rough sets, developed by Zdzisław Pawlak [12], are an important tool to describe the state of incomplete or partially unknown information. In this article, which is essentially the continuation of [8], we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library [11]). Here we drop the classical equivalence- and tolerance-based models of rough sets trying to formalize some parts of [18].

The main aim of this Mizar article is to provide a formal counterpart for the rest of the paper of William Zhu [18]. In order to do this, we recall also Theorem 3 from Y.Y. Yao’s paper [17]. The first part of our formalization (covering first seven pages) is contained in [8]. Now we start from page 5003, sec. 3.4. [18]. We formalized almost all numbered items (definitions, propositions, theorems, and corollaries), with the exception of Proposition 7, where we stated our theorem only in terms of singletons. We provided more thorough discussion of the property *positive alliance* and its connection with seriality and reflexivity (and also transitivity). Examples were not covered as a rule as we tried to construct a more general mechanism of finding appropriate models for approximation spaces in Mizar providing more automatization than it is now [10].

Of course, we can see some more general applications of some registrations of clusters, essentially not dealing with the notion of an approximation: the notions of an alliance binary relation were not defined in the Mizar Mathematical Library before, and we should think about other properties which are also absent but needed in the context of rough approximations [9], [5]. Via theory merging, using mechanisms described in [6] and [7], such elementary constructions can be extended to other frameworks.

###### Conway's Games and Some of their Basic Properties

## Conway's Games and Some of their Basic Properties

We formulate a few basic concepts of J. H. Conway's theory of games based on his book [6]. This is a first step towards formalizing Conway's theory of numbers into Mizar, which is an approach to proving the existence of a FIELD (i.e., a proper class that satisfies the axioms of a real-closed field) that includes the reals and ordinals, thus providing a uniform, independent and simple approach to these two constructions that does not go via the rational numbers and hence does for example not need the notion of a quotient field.

In this first article on Conway's games, we provide a definition of games, their birthdays (or ranks), their trees (a notion which is not in Conway's book, but is useful as a tool), their negates and their signs, together with some elementary properties of these notions. If one is interested only in Conway's numbers, it would have been easier to define them directly, but going via the notion of a game is a more general approach in the sense that a number is a special instance of a game and that there is a rich theory of games that are not numbers.

The main obstacle in formulating these topics in Mizar is that all definitions are highly recursive, which is not entirely simple to translate into the Mizar language. For example, according to Conway's definition, a game is an object consisting of left and right options which are themselves games, and this is by definition the only way to construct a game. This cannot directly be translated into Mizar, but a theorem is included in the article which proves that our definition is equivalent to Conway's.

###### On an Algorithmic Algebra over Simple-Named Complex-Valued Nominative Data

## Summary

This paper continues formalization in the Mizar system [2, 1] of basic notions of the composition-nominative approach to program semantics [14] which was started in [8, 12, 10].

The composition-nominative approach studies mathematical models of computer programs and data on various levels of abstraction and generality and provides tools for reasoning about their properties. In particular, data in computer systems are modeled as nominative data [15]. Besides formalization of semantics of programs, certain elements of the composition-nominative approach were applied to abstract systems in a mathematical systems theory [4, 6, 7, 5, 3].

In the paper we give a formal definition of the notions of a binominative function over given sets of names and values (i.e. a partial function which maps simple-named complex-valued nominative data to such data) and a nominative predicate (a partial predicate on simple-named complex-valued nominative data). The sets of such binominative functions and nominative predicates form the carrier of the generalized Glushkov algorithmic algebra for simple-named complex-valued nominative data [15]. This algebra can be used to formalize algorithms which operate on various data structures (such as multidimensional arrays, lists, etc.) and reason about their properties.

In particular, we formalize the operations of this algebra which require a specification of a data domain and which include the existential quantifier, the assignment composition, the composition of superposition into a predicate, the composition of superposition into a binominative function, the name checking predicate. The details on formalization of nominative data and the operations of the algorithmic algebra over them are described in [11, 13, 9].