- Journal Details
- Format
- Journal
- eISSN
- 1898-9934
- ISSN
- 1426-2630
- First Published
- 09 Jun 2008
- Publication timeframe
- 4 times per year
- Languages
- English

#### Search

Open Access

#### Renamings and a Condition-free Formalization of Kronecker’s Construction

Page range: 129 - 135

#### Abstract

In [7], [9], [10] we presented a formalization of Kronecker’s construction of a field extension

In this article, by means of Mizar system [2], [1], we first analyze whether our formalization can be extended that way. Using the field of polynomials over _{n }

For the general case we then introduce renamings of sets

#### Keywords

- roots of polynomials
- field extensions
- Kronecker’s construction

#### MSC 2010

- 12E05
- 12F05
- 68V20

Open Access

#### Refined Finiteness and Degree Properties in Graphs

Page range: 137 - 154

#### Abstract

In this article the finiteness of graphs is refined and the minimal and maximal degree of graphs are formalized in the Mizar system [3], based on the formalization of graphs in [4].

#### Keywords

- graph theory
- vertex degree
- maximum degree
- minimum degree

#### MSC 2010

- 68V20
- 05C07

#### Abstract

In this article the union and intersection of a set of graphs are formalized in the Mizar system [5], based on the formalization of graphs in [7].

#### Keywords

- graph theory
- graph union
- graph intersection

#### MSC 2010

- 68V20
- 05C76

Open Access

#### Unification of Graphs and Relations in Mizar

Page range: 173 - 186

#### Abstract

A (di)graph without parallel edges can simply be represented by a binary relation of the vertices and on the other hand, any binary relation can be expressed as such a graph. In this article, this correspondence is formalized in the Mizar system [2], based on the formalization of graphs in [6] and relations in [11], [12]. Notably, a new definition of createGraph will be given, taking only a non empty set

#### Keywords

- graph theory
- binary relation

#### MSC 2010

- 05C62
- 68V20

Open Access

#### Partial Correctness of a Fibonacci Algorithm

Page range: 187 - 196

#### Abstract

In this paper we introduce some notions to facilitate formulating and proving properties of iterative algorithms encoded in nominative data language [19] in the Mizar system [3], [1]. It is tested on verification of the partial correctness of an algorithm computing

#### Keywords

- nominative data
- program verification
- Fibonacci sequence

#### MSC 2010

- 68Q60
- 03B70
- 03B35

Open Access

#### Multiplication-Related Classes of Complex Numbers

Page range: 197 - 210

#### Abstract

The use of registrations is useful in shortening Mizar proofs [1], [2], both in terms of formalization time and article space. The proposed system of classes for complex numbers aims to facilitate proofs involving basic arithmetical operations and order checking. It seems likely that the use of self-explanatory adjectives could also improve legibility of these proofs, which would be an important achievement [3]. Additionally, some potentially useful definitions, following those defined for real numbers, are introduced.

#### Keywords

- complex numbers
- multiplication
- order

#### MSC 2010

- 40-04
- 68V20

#### Abstract

The foundation of the Mizar Mathematical Library [2], is first-order Tarski-Grothendieck set theory. However, the foundation explicitly refers only to Tarski’s Axiom A, which states that for every set

First we prove in Theorem (17) that every Grothendieck universe satisfies Tarski’s Axiom A. Then in Theorem (18) we prove that every Grothendieck universe that contains a given set

Then we show in Theorem (19) that Tarski-Class

The formalisation is an extension of the formalisation used in [4].

#### Keywords

- Tarski-Grothendieck set theory
- Tarski’s Axiom A
- Grothendieck universe

#### MSC 2010

- 03E70
- 68V20

#### Abstract

The main aim of this article is to introduce formally one of the generalizations of lattices, namely quasilattices, which can be obtained from the axiomatization of the former class by certain weakening of ordinary absorption laws. We show propositions QLT-1 to QLT-7 from [15], presenting also some short variants of corresponding axiom systems. Some of the results were proven in the Mizar [1], [2] system with the help of Prover9 [14] proof assistant.

#### Keywords

- lattice theory
- quasilattice
- absorption law

#### MSC 2010

- 68V20
- 06B05
- 06B75