Search Results

1 - 10 of 35 items :

Clear All


Binary representation of integers [5], [3] and arithmetic operations on them have already been introduced in Mizar Mathematical Library [8, 7, 6, 4]. However, these articles formalize the notion of integers as mapped into a certain length tuple of boolean values.

In this article we formalize, by means of Mizar system [2], [1], the binary representation of natural numbers which maps ℕ into bitstreams.


Rough sets, developed by Pawlak [15], are important tool to describe situation of incomplete or partially unknown information. In this article, continuing the formalization of rough sets [12], we give the formal characterization of three rough inclusion functions (RIFs). We start with the standard one, κ£, connected with Łukasiewicz [14], and extend this research for two additional RIFs: κ 1, and κ 2, following a paper by Gomolińska [4], [3]. We also define q-RIFs and weak q-RIFs [2]. The paper establishes a formal counterpart of [7] and makes a preliminary step towards rough mereology [16], [17] in Mizar [13].


In this article, we prove, using the Mizar [2] formalism, a number of properties that correspond to the AIM Conjecture. In the first section, we define division operations on loops, inner mappings T, L and R, commutators and associators and basic attributes of interest. We also consider subloops and homomorphisms. Particular subloops are the nucleus and center of a loop and kernels of homomorphisms. Then in Section 2, we define a set Mlt Q of multiplicative mappings of Q and cosets (mostly following Albert 1943 for cosets [1]). Next, in Section 3 we define the notion of a normal subloop and construct quotients by normal subloops. In the last section we define the set InnAut of inner mappings of Q, define the notion of an AIM loop and relate this to the conditions on T, L, and R defined by satisfies TT, etc. We prove in Theorem (67) that the nucleus of an AIM loop is normal and finally in Theorem (68) that the AIM Conjecture follows from knowing every AIM loop satisfies aa1, aa2, aa3, Ka, aK1, aK2 and aK3.

The formalization follows M.K. Kinyon, R. Veroff, P. Vojtechovsky [4] (in [3]) as well as Veroff’s Prover9 files.


In this article, we formalize in Mizar [1], [2] a binary operation of points on an elliptic curve over GF(p) in affine coordinates. We show that the operation is unital, complementable and commutative. Elliptic curve cryptography [3], whose security is based on a difficulty of discrete logarithm problem of elliptic curves, is important for information security.


In [6] partial graph mappings were formalized in the Mizar system [3]. Such mappings map some vertices and edges of a graph to another while preserving adjacency. While this general approach is appropriate for the general form of (multidi)graphs as introduced in [7], a more specialized version for graphs without parallel edges seems convenient. As such, partial vertex mappings preserving adjacency between the mapped verticed are formalized here.


Drawing a finite graph is usually done by a finite sequence of the following three operations.

1. Draw a vertex of the graph.

2. Draw an edge between two vertices of the graph.

3. Draw an edge starting from a vertex of the graph and immediately draw a vertex at the other end of it.

By this procedure any finite graph can be constructed. This property of graphs is so obvious that the author of this article has yet to find a reference where it is mentioned explicitly. In introductionary books (like [10], [5], [9]) as well as in advanced ones (like [4]), after the initial definition of graphs the examples are usually given by graphical representations rather than explicit set theoretic descriptions, assuming a mutual understanding how the representation is to be translated into a description fitting the definition. However, Mizar [2], [3] does not possess this innate ability of humans to translate pictures into graphs. Therefore, if one wants to create graphs in Mizar without directly providing a set theoretic description (i.e. using the createGraph functor), a rigorous approach to the constructing operations is required.

In this paper supergraphs are defined as an inverse mode to subgraphs as given in [8]. The three graph construction operations are defined as modes extending Supergraph similar to how the various remove operations were introduced as submodes of Subgraph in [8]. Many theorems are proven that describe how graph properties are transferred to special supergraphs. In particular, to prove that disconnected graphs cannot become connected by adding an edge between two vertices that lie in the same component, the theory of replacing a part of a walk with another walk is introduced in the preliminaries.


In the previous article [5] supergraphs and several specializations to formalize the process of drawing graphs were introduced. In this paper another such operation is formalized in Mizar [1], [2]: drawing a vertex and then immediately drawing edges connecting this vertex with a subset of the other vertices of the graph. In case the new vertex is joined with all vertices of a given graph G, this is known as the join of G and the trivial loopless graph K 1. While the join of two graphs is known and found in standard literature (like [9], [4], [8] and [3]), the operation discribed in this article is not.

Alongside the new operation a mode to reverse the directions of a subset of the edges of a graph is introduced. When all edge directions of a graph are reversed, this is commonly known as the converse of a (directed) graph.


Even and odd numbers appear early in history of mathematics [9], as they serve to describe the property of objects easily noticeable by human eye [7]. Although the use of parity allowed to discover irrational numbers [6], there is a common opinion that this property is “not rich enough to become the main content focus of any particular research” [9].

On the other hand, due to the use of decimal system, divisibility by 2 is often regarded as the property of the last digit of a number (similarly to divisibility by 5, but not to divisibility by any other primes), which probably restricts its use for any advanced purposes.

The article aims to extend the definition of parity towards its notion in binary representation of integers, thus making an alternative to the articles grouped in [5], [4], and [3] branches, formalized in Mizar [1], [2].


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].


The main purpose of formalization is to prove that two equations ya(z)= y, y = xz are Diophantine. These equations are explored in the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.

In our previous work [6], we showed that from the diophantine standpoint these equations can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities. In this formalization, we express these relations in terms of Diophantine set introduced in [7]. We prove that these relations are Diophantine and then we prove several second-order theorems that provide the ability to combine Diophantine relation using conjunctions and alternatives as well as to substitute the right-hand side of a given Diophantine equality as an argument in a given Diophantine relation. Finally, we investigate the possibilities of our approach to prove that the two equations, being the main purpose of this formalization, are Diophantine.

The formalization by means of Mizar system [3], [2] follows Z. Adamowicz, P. Zbierski [1] as well as M. Davis [4].