Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 21

Liczba wyników na stronie
first rewind previous Strona / 2 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 2 next fast forward last
1
Content available remote

Dual Lattice of ℤ-module Lattice

100%
Futa Y., Shidama Y.
Formalized Mathematics
|
2017
|
tom 25
|
nr 2
157-169
EN
In this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [20], [10] and [19].
2
Content available remote

Isomorphism Theorem on Vector Spaces over a Ring

100%
Futa Y., Shidama Y.
Formalized Mathematics
|
2017
|
tom 25
|
nr 3
171-178
EN
In this article, we formalize in the Mizar system [1, 4] some properties of vector spaces over a ring. We formally prove the first isomorphism theorem of vector spaces over a ring. We also formalize the product space of vector spaces. ℤ-modules are useful for lattice problems such as LLL (Lenstra, Lenstra and Lovász) [5] base reduction algorithm and cryptographic systems [6, 2].
3
Content available remote

Embedded Lattice and Properties of Gram Matrix

100%
Futa Y., Shidama Y.
Formalized Mathematics
|
2017
|
tom 25
|
nr 1
73-86
EN
In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded module. We also formalize properties of Gram matrix. We formally prove that an inverse of Gram matrix for a rational lattice exists. Lattice of Z-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm [16] and cryptographic systems with lattice [17].
4
Content available remote

Divisible ℤ-modules

100%
Futa Y., Shidama Y.
Formalized Mathematics
|
2016
|
tom 24
|
nr 1
37-47
EN
In this article, we formalize the definition of divisible ℤ-module and its properties in the Mizar system [3]. We formally prove that any non-trivial divisible ℤ-modules are not finitely-generated.We introduce a divisible ℤ-module, equivalent to a vector space of a torsion-free ℤ-module with a coefficient ring ℚ. ℤ-modules are important for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [15], cryptographic systems with lattices [16] and coding theory [8].
5
Content available remote

Lattice of ℤ-module

100%
Futa Y., Shidama Y.
Formalized Mathematics
|
2016
|
tom 24
|
nr 1
49-68
EN
In this article, we formalize the definition of lattice of ℤ-module and its properties in the Mizar system [5].We formally prove that scalar products in lattices are bilinear forms over the field of real numbers ℝ. We also formalize the definitions of positive definite and integral lattices and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [14], and cryptographic systems with lattices [15] and coding theory [9].
6
Content available remote

Polynomially Bounded Sequences and Polynomial Sequences

100%
Okazaki H., Futa Y.
Formalized Mathematics
|
2015
|
tom 23
|
nr 3
205-213
EN
In this article, we formalize polynomially bounded sequences that plays an important role in computational complexity theory. Class P is a fundamental computational complexity class that contains all polynomial-time decision problems [11], [12]. It takes polynomially bounded amount of computation time to solve polynomial-time decision problems by the deterministic Turing machine. Moreover we formalize polynomial sequences [5].
7
Content available remote

Z-modules

81%
Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
47-59
EN
In this article, we formalize Z-module, that is a module over integer ring. Z-module is necassary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm and cryptographic systems with lattices [11].
8
Content available remote

Operations of Points on Elliptic Curve in Projective Coordinates

81%
Futa Y., Okazaki H., Mizushima D., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
87-95
EN
In this article, we formalize operations of points on an elliptic curve over GF(p). Elliptic curve cryptography [7], whose security is based on a difficulty of discrete logarithm problem of elliptic curves, is important for information security. We prove that the two operations of points: compellProjCo and addellProjCo are unary and binary operations of a point over the elliptic curve.
9
Content available remote

Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module

81%
Nakasho K., Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2014
|
tom 22
|
nr 3
189-198
EN
In this article, we formalize some basic facts of Z-module. In the first section, we discuss the rank of submodule of Z-module and its properties. Especially, we formally prove that the rank of any Z-module is equal to or more than that of its submodules, and vice versa, and that there exists a submodule with any given rank that satisfies the above condition. In the next section, we mention basic facts of linear transformations between two Z-modules. In this section, we define homomorphism between two Z-modules and deal with kernel and image of homomorphism. In the last section, we formally prove some basic facts about linearly independent subsets and linear combinations. These formalizations are based on [9](p.191-242), [23](p.117-172) and [2](p.17-35).
10
Content available remote

Set of Points on Elliptic Curve in Projective Coordinates

81%
Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2011
|
tom 19
|
nr 3
131-138
EN
In this article, we formalize a set of points on an elliptic curve over GF(p). Elliptic curve cryptography [10], whose security is based on a difficulty of discrete logarithm problem of elliptic curves, is important for information security.
11
Content available remote

Topological Properties of Real Normed Space

81%
Nakasho K., Futa Y., Shidama Y.
Formalized Mathematics
|
2014
|
tom 22
|
nr 3
209-223
EN
In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered here. Then we argue the condition when real normed subspaces become Banach’s spaces. We also formalize quotient vector space. In the last session, we argue the properties of the closure of real normed space. These formalizations are based on [19](p.3-41), [2] and [34](p.3-67).
12
Content available remote

Torsion Z-module and Torsion-free Z-module

81%
Futa Y., Okazaki H., Nakasho K., Shidama Y.
Formalized Mathematics
|
2014
|
tom 22
|
nr 4
277-289
EN
In this article, we formalize a torsion Z-module and a torsionfree Z-module. Especially, we prove formally that finitely generated torsion-free Z-modules are finite rank free. We also formalize properties related to rank of finite rank free Z-modules. The notion of Z-module is necessary for solving lattice problems, LLL (Lenstra, Lenstra, and Lov´asz) base reduction algorithm [20], cryptographic systems with lattice [21], and coding theory [11].
13
Content available remote

Matrix of ℤ-module1

81%
Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2015
|
tom 23
|
nr 1
29-49
EN
In this article, we formalize a matrix of ℤ-module and its properties. Specially, we formalize a matrix of a linear transformation of ℤ-module, a bilinear form and a matrix of the bilinear form (Gramian matrix). We formally prove that for a finite-rank free ℤ-module V, determinant of its Gramian matrix is constant regardless of selection of its basis. ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattices [22] and coding theory [14]. Some theorems in this article are described by translating theorems in [24], [26] and [19] into theorems of ℤ-module.
14
Content available remote

Formalization of Integral Linear Space

81%
Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2011
|
tom 19
|
nr 1
61-64
EN
In this article, we formalize integral linear spaces, that is a linear space with integer coefficients. Integral linear spaces are necessary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm that outputs short lattice base and cryptographic systems with lattice [8].
15
Content available remote

Quotient Module of Z-module

81%
Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 3
205-214
EN
In this article we formalize a quotient module of Z-module and a vector space constructed by the quotient module. We formally prove that for a Z-module V and a prime number p, a quotient module V/pV has the structure of a vector space over Fp. Z-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm and cryptographic systems with lattices [14]. Some theorems in this article are described by translating theorems in [20] and [19] into theorems of Z-module.
16
Content available remote

Free ℤ-module

81%
Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 4
275-280
EN
In this article we formalize a free ℤ-module and its rank. We formally prove that for a free finite rank ℤ-module V , the number of elements in its basis, that is a rank of the ℤ-module, is constant regardless of the selection of its basis. ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [15]. Some theorems in this article are described by translating theorems in [21] and [8] into theorems of Z-module.
17
Content available remote

Gaussian Integers

81%
Futa Y., Okazaki H., Mizushima D., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 2
115-125
EN
Gaussian integer is one of basic algebraic integers. In this article we formalize some definitions about Gaussian integers [27]. We also formalize ring (called Gaussian integer ring), Z-module and Z-algebra generated by Gaussian integer mentioned above. Moreover, we formalize some definitions about Gaussian rational numbers and Gaussian rational number field. Then we prove that the Gaussian rational number field and a quotient field of the Gaussian integer ring are isomorphic.
18
Content available remote

Constructing Binary Huffman Tree

81%
Okazaki H., Futa Y., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 2
133-143
EN
Huffman coding is one of a most famous entropy encoding methods for lossless data compression [16]. JPEG and ZIP formats employ variants of Huffman encoding as lossless compression algorithms. Huffman coding is a bijective map from source letters into leaves of the Huffman tree constructed by the algorithm. In this article we formalize an algorithm constructing a binary code tree, Huffman tree.
19
Content available remote

Isometric Differentiable Functions on Real Normed Space

81%
Futa Y., Endou N., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 4
249-260
EN
In this article, we formalize isometric differentiable functions on real normed space [17], and their properties.
20
Content available remote

Submodule of free Z-module

81%
Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 4
273-282
EN
In this article, we formalize a free Z-module and its property. In particular, we formalize the vector space of rational field corresponding to a free Z-module and prove formally that submodules of a free Z-module are free. Z-module is necassary for lattice problems - LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm and cryptographic systems with lattice [20]. Some theorems in this article are described by translating theorems in [11] into theorems of Z-module, however their proofs are different.
first rewind previous Strona / 2 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.