Hiroyuki Okazaki

Formaliz. Math., September, 2023

2022

Formalization of Orthogonal Decomposition for Hilbert Spaces.

[BibT_eX]

[DOI]

Formaliz. Math., December, 2022

2021

The 3-Fold Product Space of Real Normed Spaces and its Properties.

[BibT_eX]

[DOI]

Kazuhisa Nakasho

Formaliz. Math., 2021

Finite Dimensional Real Normed Spaces are Proper Metric Spaces.

[BibT_eX]

[DOI]

Kazuhisa Nakasho

Formaliz. Math., 2021

Real Vector Space and Related NotionsThis study was supported in part by JSPS KAKENHI Grant Numbers 17K00182 and 20K19863.

[BibT_eX]

[DOI]

Kazuhisa Nakasho

Formaliz. Math., 2021

Virtual Environment for Analysis and Evaluation of DDoS Attacks.

[BibT_eX]

[DOI]

Proceedings of the Advanced Information Networking and Applications, 2021

2020

Formal Verification of Merkle-Damgård Construction in ProVerif.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Information Theory and Its Applications, 2020

2019

Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm.

[BibT_eX]

[DOI]

Koh-ichi Nagao

Formaliz. Math., 2019

Operations of Points on Elliptic Curve in Affine Coordinates.

[BibT_eX]

[DOI]

Formaliz. Math., 2019

2018

Binary Representation of Natural Numbers.

[BibT_eX]

[DOI]

Formaliz. Math., 2018

Suitable Symbolic Models for Cryptographic Verification of Secure Protocols in ProVerif.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Information Theory and Its Applications, 2018

2016

Conservation Rules of Direct Sum Decomposition of Groups.

[BibT_eX]

[DOI]

Formaliz. Math., 2016

Privacy Preserving Logic Formula Calculation in Cloud.

[BibT_eX]

[DOI]

Proceedings of the Tenth IEEE International Conference on Semantic Computing, 2016

Formalization of statistical indistinguishability of probability distribution ensembles in Mizar.

[BibT_eX]

[DOI]

Proceedings of the 2016 International Symposium on Information Theory and Its Applications, 2016

Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar.

[BibT_eX]

[DOI]

Proceedings of the Joint Proceedings of the FM4M, 2016

2015

Polynomially Bounded Sequences and Polynomial Sequences.

[BibT_eX]

[DOI]

Formaliz. Math., 2015

Algebra of Polynomially Bounded Sequences and Negligible Functions.

[BibT_eX]

[DOI]

Formaliz. Math., 2015

Definition and Properties of Direct Sum Decomposition of Groups1.

[BibT_eX]

[DOI]

Formaliz. Math., 2015

Equivalent Expressions of Direct Sum Decomposition of Groups1.

[BibT_eX]

[DOI]

Formaliz. Math., 2015

Torsion Part of ℤ-module.

[BibT_eX]

[DOI]

Formaliz. Math., 2015

Matrix of ℤ-module1.

[BibT_eX]

[DOI]

Formaliz. Math., 2015

Application to Women's Healthcare of Health Management System Using a Tablet Phone.

[BibT_eX]

[DOI]

Proceedings of the Brain Informatics and Health - 8th International Conference, 2015

2014

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

[BibT_eX]

[DOI]

Formaliz. Math., 2014

Torsion Z-module and Torsion-free Z-module.

[BibT_eX]

[DOI]

Formaliz. Math., 2014

Difference of Function on Vector Space over F.

[BibT_eX]

[DOI]

Ken Wakabayashi

Formaliz. Math., 2014

2013

Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order.

[BibT_eX]

[DOI]

Formaliz. Math., 2013

Isomorphisms of Direct Products of Finite Commutative Groups.

[BibT_eX]

[DOI]

Hiroshi Yamazaki

Formaliz. Math., 2013

Random Variables and Product of Probability Spaces.

[BibT_eX]

[DOI]

Formaliz. Math., 2013

Constructing Binary Huffman Tree.

[BibT_eX]

[DOI]

Formaliz. Math., 2013

The Ck Space.

[BibT_eX]

[DOI]

Katuhiko Kanazashi

Formaliz. Math., 2013

Submodule of free Z-module.

[BibT_eX]

[DOI]

Formaliz. Math., 2013

Gaussian Integers.

[BibT_eX]

[DOI]

Formaliz. Math., 2013

Double Sequences and Limits.

[BibT_eX]

[DOI]

Formaliz. Math., 2013

Formalization of the Advanced Encryption Standard. Part I.

[BibT_eX]

[DOI]

Formaliz. Math., 2013

N-Dimensional Binary Vector Spaces.

[BibT_eX]

[DOI]

Formaliz. Math., 2013

Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar.

[BibT_eX]

[DOI]

Artif. Intell. Res., 2013

2012

Banach's Continuous Inverse Theorem and Closed Graph Theorem.

[BibT_eX]

[DOI]

Hideki Sakurai

Formaliz. Math., 2012

Formalization of the Data Encryption Standard.

[BibT_eX]

[DOI]

Formaliz. Math., 2012

Extended Euclidean Algorithm and CRT Algorithm.

[BibT_eX]

[DOI]

Yosiki Aoki

Formaliz. Math., 2012

Posterior Probability on Finite Set.

[BibT_eX]

[DOI]

Formaliz. Math., 2012

Functional Space C(ω), C0(ω).

[BibT_eX]

[DOI]

Katuhiko Kanazashi

Formaliz. Math., 2012

Free ℤ-module.

[BibT_eX]

[DOI]

Formaliz. Math., 2012

Quotient Module of Z-module.

[BibT_eX]

[DOI]

Formaliz. Math., 2012

Z-modules.

[BibT_eX]

[DOI]

Formaliz. Math., 2012

Operations of Points on Elliptic Curve in Projective Coordinates.

[BibT_eX]

[DOI]

Formaliz. Math., 2012

Higher-Order Partial Differentiation.

[BibT_eX]

[DOI]

Formaliz. Math., 2012

Isomorphisms of Direct Products of Finite Cyclic Groups.

[BibT_eX]

[DOI]

Formaliz. Math., 2012

Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar.

[BibT_eX]

[DOI]

Daichi Mizushima

Proceedings of the International Symposium on Information Theory and its Applications, 2012

2011

Cartesian Products of Family of Real Linear Spaces.

[BibT_eX]

[DOI]

Formaliz. Math., 2011

More on Continuous Functions on Normed Linear Spaces.

[BibT_eX]

[DOI]

Formaliz. Math., 2011

Differentiable Functions into Real Normed Spaces.

[BibT_eX]

[DOI]

Formaliz. Math., 2011

Normal Subgroup of Product of Groups.

[BibT_eX]

[DOI]

Formaliz. Math., 2011

Banach Algebra of Bounded Complex-Valued Functionals.

[BibT_eX]

[DOI]

Katuhiko Kanazashi

Formaliz. Math., 2011

Set of Points on Elliptic Curve in Projective Coordinates.

[BibT_eX]

[DOI]

Formaliz. Math., 2011

Formalization of Integral Linear Space.

[BibT_eX]

[DOI]

Formaliz. Math., 2011

2010

Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables.

[BibT_eX]

[DOI]

Formaliz. Math., 2010

Formalization of Probability and Random Sampling on a Finite and Discrete Sample Space Using the Mizar Proof Checker.

[BibT_eX]

Nobuaki Kondo

Proceedings of the 2010 International Conference on Foundations of Computer Science, 2010

2009

Probability on Finite Set and Real-Valued Random Variables.

[BibT_eX]

[DOI]

Formaliz. Math., 2009

Probability on Finite and Discrete Set and Uniform Distribution.

[BibT_eX]

[DOI]

Formaliz. Math., 2009

Hopf Extension Theorem of Measure.

[BibT_eX]

[DOI]

Formaliz. Math., 2009

Properties of Primes and Multiplicative Group of a Field.

[BibT_eX]

[DOI]

Formaliz. Math., 2009

2008

Uniqueness of Factoring an Integer and Multiplicative Group Z/pZ*.

[BibT_eX]

[DOI]

Formaliz. Math., 2008

2007

An evolutionary multiobjective approach to design highly non-linear Boolean functions.

[BibT_eX]

[DOI]

Hernán E. Aguirre

Yasushi Fuwa

Proceedings of the Genetic and Evolutionary Computation Conference, 2007

2005

Meta Ring Signature.

[BibT_eX]

[DOI]