- 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
Triviality of fundamental groups of spheres of dimension greater than 1 is proven, [17]
Abstract
The Borsuk-Ulam theorem about antipodals is proven, [18, pp. 32-33].
Abstract
In this article, we shall extend the formalization of [10] to discuss higher-order partial differentiation of real valued functions. The linearity of this operator is also proved (refer to [10], [12] and [13] for partial differentiation).
- Open Access
Formalization of the Data Encryption Standard
Page range: 125 - 146
Abstract
In this article we formalize DES (the Data Encryption Standard), that was the most widely used symmetric cryptosystem in the world. DES is a block cipher which was selected by the National Bureau of Standards as an official Federal Information Processing Standard for the United States in 1976 [15].
Abstract
In the paper the semantics of MML Query queries is given. The formalization is done according to [4]
- Open Access
Routh’s, Menelaus’ and Generalized Ceva’s Theorems
Page range: 157 - 159
Abstract
The goal of this article is to formalize Ceva’s theorem that is in the [8] on the web. Alongside with it formalizations of Routh’s, Menelaus’ and generalized form of Ceva’s theorem itself are provided.
- Open Access
Simple Graphs as Simplicial Complexes: the Mycielskian of a Graph
Page range: 161 - 174
Abstract
Harary [10, p. 7] claims that Veblen [20, p. 2] first suggested to formalize simple graphs using simplicial complexes. We have developed basic terminology for simple graphs as at most 1-dimensional complexes.
We formalize this new setting and then reprove Mycielski’s [12] construction resulting in a triangle-free graph with arbitrarily large chromatic number. A different formalization of similar material is in [15].
- Open Access
Extended Euclidean Algorithm and CRT Algorithm
Page range: 175 - 179
Abstract
In this article we formalize some number theoretical algorithms, Euclidean Algorithm and Extended Euclidean Algorithm [9]. 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 [8].
Abstract
In this article we formalize rational functions as pairs of polynomials and define some basic notions including the degree and evaluation of rational functions [8]. The main goal of the article is to provide properties of rational functions necessary to prove a theorem on the stability of networks