The Mizar system is one of the pioneering systems aimed at supporting mathematical proof
development on a computer that have laid the groundwork for and eventually have evolved …

Mathematics, especially algebra, uses plenty of structures: groups, rings, integral domains,
fields, vector spaces to name a few of the most basic ones. Classes of structures are closely …

We describe a formalization of the nominative algorithmic algebra in the Mizar proof
assistant. This algebra is a generalization of Glushkov algorithmic algebras which is well …

In the paper we describe a formalization of the notion of a nominative data with simple
names and complex values in the Mizar proof assistant. Such data can be considered as a …

Our work is focused on the Mizar proof assistant and accessing the contents of its library in a
machine readable and easily accessible form. The main result of the work described here is …

In the paper, we discuss the formal approach to Tarski geometry axioms modelled with the
help of the Mizar computerized proof assistant system. Although our basic development was …

The Mizar language and its corresponding proof-checker offers the tactic of definitional
expansions in proof skeletons. This apparatus is rather fragile in the case of intensive …

Abstract The classical Floyd-Hoare logic is defined for the case of total pre-and
postconditions and partial programs (ie programs can be undefined on some input data, but …

The Mizar Mathematical Library is one of the largest collections of machine understandable
formal proofs encompassing many areas of today mathematics including results from …

The main aim of this article is to construct two non-trivial examples of weakly associative
lattices (also known as trellises). These are generalizations of lattices, not assuming …