Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order. - Hiroshi Yamazaki; Hiroyuki Okazaki; Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2013)

Torsion Z-module and Torsion-free Z-module. - Yuichi Futa; Hiroyuki Okazaki; Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2014)

Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module. - Kazuhisa Nakasho; Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2014)

Topological Properties of Real Normed Space. - Kazuhisa Nakasho; Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2014)

Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library. - Kazuhisa Nakasho; Yasunari Shidama (CICM, 2015)

σ-ring and σ-algebra of Sets1. - Noboru Endou; Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2015)

Separability of Real Normed Spaces and Its Basic Properties. - Kazuhisa Nakasho; Noboru Endou (Formaliz. Math., 2015)

Equivalent Expressions of Direct Sum Decomposition of Groups1. - Kazuhisa Nakasho; Hiroyuki Okazaki; Hiroshi Yamazaki; Yasunari Shidama (Formaliz. Math., 2015)

Definition and Properties of Direct Sum Decomposition of Groups1. - Kazuhisa Nakasho; Hiroshi Yamazaki; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2015)

Implementation of a vital signs monitoring system in combination with a bed-leaving detection system. - Kazuhisa Nakasho; Hirokazu Madokoro; Nobuhiro Shimoi (SII, 2016)

Compactness in Metric Spaces. - Kazuhisa Nakasho; Keiko Narita; Yasunari Shidama (Formaliz. Math., 2016)

The Basic Existence Theorem of Riemann-Stieltjes Integral. - Kazuhisa Nakasho; Keiko Narita; Yasunari Shidama (Formaliz. Math., 2016)

Conservation Rules of Direct Sum Decomposition of Groups. - Kazuhisa Nakasho; Hiroshi Yamazaki; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2016)

Riemann-Stieltjes Integral. - Keiko Narita; Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2016)

Unsupervised learning-based semantic scene recognition and boundary visualization on category maps. - Hirokazu Madokoro; Kazuhito Sato; Kazuhisa Nakasho; Nobuhiro Shimoi (ICDL-EPIROB, 2017)

Adaptive learning based driving episode description on category maps. - Hirokazu Madokoro; Kazuhito Sato; Kazuhisa Nakasho; Nobuhiro Shimoi (IJCNN, 2017)

Context based semantic scene classification and recognition used for a vision-based mobile robot. - Hirokazu Madokoro; Kazuhito Sato; Kazuhisa Nakasho; Nobuhiro Shimoi (RO-MAN, 2017)

Implicit Function Theorem. Part I. - Kazuhisa Nakasho; Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2017)

F. Riesz Theorem. - Keiko Narita; Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2017)

Privacy-Preserving Integration of Medical Data - A Practical Multiparty Private Set Intersection. - Atsuko Miyaji; Kazuhisa Nakasho; Shohei Nishida (J. Medical Syst., 2017)

Development of a Secure Cross-Institutional Data Collection System Based on Distributed Standardized EMR Storage. - Katsuya Tanaka; Ryuichi Yamamoto; Kazuhisa Nakasho; Atsuko Miyaji (EFMI-STC, 2018)

Continuity of Bounded Linear Operators on Normed Linear Spaces. - Kazuhisa Nakasho; Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2018)

Development of a Flexible Mizar Tokenizer and Parser for Information Retrieval System. - Kazuhisa Nakasho (FedCSIS, 2019)

Bilinear Operators on Normed Linear Spaces. - Kazuhisa Nakasho (Formaliz. Math., 2019)

Multilinear Operator and Its Basic Properties. - Kazuhisa Nakasho (Formaliz. Math., 2019)

Isomorphisms from the Space of Multilinear Operators. - Kazuhisa Nakasho (Formaliz. Math., 2019)

Invertible Operators on Banach Spaces. - Kazuhisa Nakasho (Formaliz. Math., 2019)

Continuity of Multilinear Operator on Normed Linear Spaces. - Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2019)

Implicit Function Theorem. Part II. - Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2019)

Secure Primitive for Big Data Utilization. - Akinori Kawachi; Atsuko Miyaji; Kazuhisa Nakasho; Yiying Qi; Yuuki Takano (Security Infrastructure Technology for Integrated Utilization of Big Data, 2020)

Development and Application of Privacy-preserving Distributed Medical Data Integration System. - Seitaro Mishima; Kazuhisa Nakasho; Kousuke Takeuchi; Naohiro Hayaishi; Yuuki Takano; Atsuko Miyaji (ICCE-TW, 2020)

Development of Invisible Sensors and a Machine-Learning-Based Recognition System Used for Early Prediction of Discontinuous Bed-Leaving Behavior Patterns. - Hirokazu Madokoro; Kazuhisa Nakasho; Nobuhiro Shimoi; Hanwool Woo; Kazuhito Sato (Sensors, 2020)

A Practical Parallel Computation in a Scalable Multiparty Private Set Intersection. - Seitaro Mishima; Kazuhisa Nakasho; Yuuki Takano; Atsuko Miyaji (CANDAR (Workshops), 2021)

Visual Studio Code Extension and Auto-completion for Mizar Language. - Hirota Taniguchi; Kazuhisa Nakasho (CANDAR, 2021)

A Web Platform for Hosting the Mizar Mathematical Library (short paper). - Daichi Yamamichi; Seigo Shigenaka; Kazuhisa Nakasho; Katsumi Wasaki (CICM Workshops, 2021)

Inverse Function Theorem. Part I1. - Kazuhisa Nakasho; Yuichi Futa (Formaliz. Math., 2021)

Real Vector Space and Related NotionsThis study was supported in part by JSPS KAKENHI Grant Numbers 17K00182 and 20K19863. - Kazuhisa Nakasho; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2021)

Finite Dimensional Real Normed Spaces are Proper Metric Spaces. - Kazuhisa Nakasho; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2021)

The 3-Fold Product Space of Real Normed Spaces and its Properties. - Hiroyuki Okazaki; Kazuhisa Nakasho (Formaliz. Math., 2021)

Classification of Human Posture on Bed Using Machine Learning. - Kenta Sawada; Kazuhisa Nakasho; Katsumi Wasaki; Nobuhiro Shimoi (ICCE-TW, 2022)

Development of an IoT Device for Structural Health Monitoring. - Keiju Seki; Kazuhisa Nakasho; Cuadra Carlos; Nobuhiro Shimoi (ICCE-TW, 2022)

An Integrated Web Platform for the Mizar Mathematical Library. - Hideharu Furushima; Daichi Yamamichi; Seigo Shigenaka; Kazuhisa Nakasho; Katsumi Wasaki (CICM, 2022)

Transformation Tools for Real Linear Spaces. - Kazuhisa Nakasho (Formaliz. Math., 2022)

Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces. - Kazuhisa Nakasho; Yuichi Futa (Formaliz. Math., 2022)

On Implicit and Inverse Function Theorems on Euclidean Spaces. - Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2022)

The Tight Upper Bound for the Size of Single Deletion Error Correcting Codes in Dimension 11. - Kazuhisa Nakasho; Manabu Hagiwara; Austin Anderson; James B. Nation (CoRR, 2023)

Optimal Positioning of Sensors in a Bed Monitoring System Using RFID. - Ryota Adachi; Yu Yamauchi; Nobuhiro Shimoi; Kazuhisa Nakasho (ICCE-Taiwan, 2024)

Enhancing Learning Support Functions for Projectile Motion in the VR Application HoloThrow. - Natsumi Oshiro; Tatsuro Ueda; Kazuhisa Nakasho (ICCE-Taiwan, 2024)

Study on the Impact of Subject Variability in a Bed Monitoring System Using RFID. - Keisuke Soma; Yu Yamauchi; Nobuhiro Shimoi; Kazuhisa Nakasho (ICCE-Taiwan, 2024)

The Tight Upper Bound for the Size of Single Deletion Error Correcting Codes of Length 11. - Kazuhisa Nakasho; Manabu Hagiwara; Austin Anderson; James B. Nation (ISITA, 2024)

Remote Verification System for Mizar Integrated with Emwiki. - Toshiki Kai; Yuta Teruya; Kazuhisa Nakasho (CICM, 2024)

Differentiability Properties of Lipschitzian Bilinear Operators in Real Normed Spaces. - Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2024)

Classical Isoperimetric Theorem. - Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2024)

On the Properties of Curves and Parametrization-Independent Isoperimetric Inequality. - Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2024)

Higher-Order Differentiation and Inverse Function Theorem in Real Normed Spaces. - Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2024)