We have formalized the BCI-algebras closely following the book  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.
Rough sets, developed by Pawlak , 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 . We continue the formalization of rough sets in Mizar  started in .
Kinetic models have so far been used to model wealth distribution in a society. In particular, within the framework of the kinetic theory for active particles, some important models have been developed and proposed. They involve nonlinear interactions among individuals that are modeled according to game theoretical tools by introducing parameters governing the temporal dynamics of the system. In this present paper we propose an approach based on optimal control tools that aims to optimize this evolving dynamics from a social point of view. Namely, we look for time dependent control variables concerning the distribution of wealth that can be managed, for instance, by the government, in order to obtain a given social profile.
Hiroyuki Okazaki, Yosiki Aoki and Yasunari Shidama
In this article we formalize some number theoretical algorithms, Euclidean Algorithm and Extended Euclidean Algorithm . 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 .
Rough sets, developed by Pawlak , 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 , is also a step towards the formalization of the algebraic theory of rough sets, as in  or .
The notion of a rough set, developed by Pawlak , is an important tool to describe situation of incomplete or partially unknown information. In this article, which is essentially the continuation of , 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  trying to formalize some parts of  following also  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 , 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.
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 , 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 . We partially prove the theorem of  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  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.
Ievgen Ivanov, Artur Korniłowicz and Mykola Nikitchenko
This paper continues formalization in Mizar [2, 1] of basic notions of the composition-nominative approach to program semantics  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  over given sets form the carrier of the generalized Glushkov algorithmic algebra . 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].
Ievgen Ivanov, Artur Korniłowicz and Mykola Nikitchenko
This paper continues formalization in the Mizar system [2, 1] of basic notions of the composition-nominative approach to program semantics  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 . 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 . 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].
Giacomo Aletti, Davide Lonardoni, Giovanni Naldi and Thierry Nieus
One major challenge in neuroscience is the identification of interrelations between signals reflecting neural activity and how information processing occurs in the neural circuits. At the cellular and molecular level, mechanisms of signal transduction have been studied intensively and a better knowledge and understanding of some basic processes of information handling by neurons has been achieved. In contrast, little is known about the organization and function of complex neuronal networks. Experimental methods are now available to simultaneously monitor electrical activity of a large number of neurons in real time. Then, the qualitative and quantitative analysis of the spiking activity of individual neurons is a very valuable tool for the study of the dynamics and architecture of the neural networks. Such activity is not due to the sole intrinsic properties of the individual neural cells but it is mostly the consequence of the direct influence of other neurons. The deduction of the effective connectivity between neurons, whose experimental spike trains are observed, is of crucial importance in neuroscience: first for the correct interpretation of the electro-physiological activity of the involved neurons and neural networks, and, for correctly relating the electrophysiological activity to the functional tasks accomplished by the network. In this work, we propose a novel method for the identification of connectivity of neural networks using recorded voltages. Our approach is based on the assumption that the network has a topology with sparse connections. After a brief description of our method, we will report the performances and compare it to the cross-correlation computed on the spike trains, which represents a gold standard method in the field.