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

#### Search

#### Abstract

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

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

#### Keywords

- divisibility
- binary representation

#### MSC 2010

- 11A51
- 03B35
- 68T99

#### Abstract

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

In this paper supergraphs are defined as an inverse mode to subgraphs as given in

#### Keywords

- supergraph
- graph operations

#### MSC 2010

- 05C76
- 03B35
- 68T99

#### Abstract

In the previous article _{1}. While the join of two graphs is known and found in standard literature (like

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.

#### Keywords

- supergraph
- graph operations

#### MSC 2010

- 05C76
- 03B35
- 68T99

Open Access

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

Page range: 141 - 147

#### Abstract

This paper continues formalization in Mizar

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 [

In the paper we introduce a definition of the notion of a binominative function over a set

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

#### Keywords

- Glushkov algorithmic algebra
- uninterpreted data

#### MSC 2010

- 68Q60
- 68T37
- 03B70
- 03B35

Open Access

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

Page range: 149 - 158

#### Abstract

This paper continues formalization in the Mizar system

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

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

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 [

#### Keywords

- Glushkov algorithmic algebra
- nominative data

#### MSC 2010

- 68Q60
- 68T37
- 03B70
- 03B35

Open Access

#### An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates

Page range: 159 - 164

#### Abstract

In the paper we give a formalization in the Mizar system

We formalize the notion of a semantic Floyd-Hoare triple (for an extended Floyd-Hoare logic with partial pre- and post-conditions)

We formalize and prove the soundness of the rules of the inference system

The formalized rules can be used for reasoning about sequential programs, and in particular, for sequential programs on nominative data

#### Keywords

- Floyd-Hoare logic
- Floyd-Hoare triple
- inference rule
- program verification

#### MSC 2010

- 68Q60
- 68T37
- 03B70
- 03B35

#### Abstract

In this paper we present a formalization in the Mizar system

The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data

#### Keywords

- greatest common divisor
- nominative data
- program verification

#### MSC 2010

- 68Q60
- 68T37
- 03B70
- 03B35

#### Abstract

The main purpose of formalization is to prove that two equations y

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

The formalization by means of Mizar system

#### Keywords

- Hilbert’s 10th problem
- Diophantine relations

#### MSC 2010

- 11D45
- 03B35
- 68T99

Open Access

#### Formalizing Two Generalized Approximation Operators

Page range: 183 - 191

#### Abstract

Rough sets, developed by Pawlak

#### Keywords

- rough approximation
- rough set
- generalized approximation operator

#### MSC 2010

- 03E99
- 03B35
- 68T99

Open Access

#### On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander

Page range: 193 - 198

#### Abstract

The main result of the article is to prove formally that two sets of axioms, proposed by McKenzie and Sholander, axiomatize lattices and distributive lattices, respectively. In our Mizar article we used proof objects generated by Prover9. We continue the work started in

#### Keywords

- lattice
- distributive lattice
- lattice axioms

#### MSC 2010

- 03B35
- 68T99
- 06B05
- 06D05