REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

  1. Repozytorium Uniwersytetu w Białymstoku
  2. Czasopisma naukowe / Journals
  3. Formalized Mathematics
  4. Formalized Mathematics, 2017, Volume 25, Issue 1

Szukanie zaawansowane
  • Zespoły i Kolekcje


  • Zaloguj się
  • Zarejestruj się
  • Mój RUB
  • FAQ
  • Polityka
  • Regulamin
  • DOI
  • Instrukcja
  • Aspekty prawne
  • Open Access
  • Archiwum


  • Kontakt
  • O Dspace
  • Strona Biblioteki
  • Strona Uczelni



    • Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/5571
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorFuta, Yuichi-
    dc.contributor.authorShidama, Yasunari-
    dc.date.accessioned2017-06-05T08:32:52Z-
    dc.date.available2017-06-05T08:32:52Z-
    dc.date.issued2017-
    dc.identifier.citationFormalized Mathematics, Volume 25, Issue 1, pp. 72-86pl
    dc.identifier.issn1426-2630pl
    dc.identifier.issn1898-9934pl
    dc.identifier.urihttp://hdl.handle.net/11320/5571-
    dc.description.abstractIn 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 ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [16] and cryptographic systems with lattice [17].-
    dc.language.isoen-
    dc.publisherDe Gruyter Open-
    dc.subjectℤ-lattice-
    dc.subjectGram matrix-
    dc.subjectrational ℤ-lattice-
    dc.titleEmbedded Lattice and Properties of Gram Matrix-
    dc.typeArticle-
    dc.identifier.doi10.1515/forma-2017-0007-
    dc.description.AffiliationFuta Yuichi - Tokyo University of Technology, Tokyo, Japan-
    dc.description.AffiliationShidama Yasunari - Shinshu University, Nagano, Japan-
    dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.-
    dc.description.referencesGrzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543-547, 1990.-
    dc.description.referencesGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.-
    dc.description.referencesGrzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.-
    dc.description.referencesCzesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990.-
    dc.description.referencesCzesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.-
    dc.description.referencesCzesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.-
    dc.description.referencesCzesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.-
    dc.description.referencesYuichi Futa and Yasunari Shidama. Lattice of Z-module. Formalized Mathematics, 24 (1):49-68, 2016. doi: 10.1515/forma-2016-0005.-
    dc.description.referencesYuichi Futa and Yasunari Shidama. Divisible Z-modules. Formalized Mathematics, 24 (1):37-47, 2016. doi: 10.1515/forma-2016-0004.-
    dc.description.referencesYuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Z-modules. Formalized Mathe matics, 20(1):47-59, 2012. doi: 10.2478/v10037-012-0007-z.-
    dc.description.referencesYuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Quotient module of ℤ-module. Formalized Mathematics, 20(3):205-214, 2012.-
    dc.description.referencesYuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Matrix of ℤ-module. Formalized Mathematics, 23(1):29-49, 2015.-
    dc.description.referencesAdam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015.-
    dc.description.referencesEugeniusz Kusak, Wojciech Leonczuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.-
    dc.description.referencesA. K. Lenstra, H. W. Lenstra Jr., and L. Lov´asz. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4):515-534, 1982.-
    dc.description.referencesDaniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: a cryptographic perspective. The International Series in Engineering and Computer Science, 2002.-
    dc.description.referencesMichał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3-11, 1991.-
    dc.description.referencesKarol Pak. Basic properties of the rank of matrices over a field. Formalized Mathematics, 15(4):199-211, 2007.-
    dc.description.referencesKarol Pak and Andrzej Trybulec. Laplace expansion. Formalized Mathematics, 15(3): 143-150, 2007.-
    dc.description.referencesNobuyuki Tamura and Yatsuka Nakamura. Determinant and inverse of matrices of real elements. Formalized Mathematics, 15(3):127-136, 2007.-
    dc.description.referencesAndrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990.-
    dc.description.referencesWojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569-573, 1990.-
    dc.description.referencesWojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.-
    dc.description.referencesWojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Formalized Mathematics, 1(5):865-870, 1990.-
    dc.description.referencesWojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1 (5):877-882, 1990.-
    dc.description.referencesWojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883-885, 1990.-
    dc.description.referencesZinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.-
    dc.description.referencesEdmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.-
    Występuje w kolekcji(ach):Formalized Mathematics, 2017, Volume 25, Issue 1

    Pliki w tej pozycji:
    Plik Opis RozmiarFormat 
    forma-2017-0007.pdf299,24 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


    Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons