Showing 1–3 of 3 results for author: Nakasho, K

The Tight Upper Bound for the Size of Single Deletion Error Correcting Codes in Dimension 11

Authors: Kazuhisa Nakasho, Manabu Hagiwara, Austin Anderson, J. B. Nation

Abstract: A single deletion error correcting code (SDECC) is a set of fixed-length sequences consisting of two types of symbols, 0 and 1, such that the original sequence can be recovered for at most one deletion error. The upper bound for the size of SDECC is expected to be equal to the size of Varshamov-Tenengolts (VT) code, and this conjecture had been shown to be true when the code length is ten or less.… ▽ More A single deletion error correcting code (SDECC) is a set of fixed-length sequences consisting of two types of symbols, 0 and 1, such that the original sequence can be recovered for at most one deletion error. The upper bound for the size of SDECC is expected to be equal to the size of Varshamov-Tenengolts (VT) code, and this conjecture had been shown to be true when the code length is ten or less. In this paper, we discuss a method for calculating this upper bound by providing an integer linear programming solver with several linear constraints. As a new result, we obtained that the tight upper bound for the size of a single deletion error correcting code in dimension 11 is 172. △ Less

Submitted 26 September, 2023; originally announced September 2023.

MSC Class: 68P30 ACM Class: E.4; G.2.1

An Integrated Web Platform for the Mizar Mathematical Library

Authors: Hideharu Furushima, Daichi Yamamichi, Seigo Shigenaka, Kazuhisa Nakasho, Katsumi Wasaki

Abstract: This paper reports on the development of a Web platform to host the Mizar Mathematical Library (MML). In recent years, the size of formalized mathematical libraries has been drastically increasing, and this has led to a growing demand for tools that support efficient and comprehensive browsing, searching, and annotation of these libraries. This platform implements a Wiki function to add comments t… ▽ More This paper reports on the development of a Web platform to host the Mizar Mathematical Library (MML). In recent years, the size of formalized mathematical libraries has been drastically increasing, and this has led to a growing demand for tools that support efficient and comprehensive browsing, searching, and annotation of these libraries. This platform implements a Wiki function to add comments to the HTMLized MML, three types of search function (article, symbol, and theorem), and a function to show the dependency graph of the MML. This platform is designed with consistency, scalability, and interoperability as top priorities for long-term use. △ Less

Submitted 20 September, 2022; originally announced October 2022.

MSC Class: 68V25; 68V30; 68V35 ACM Class: G.4

Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library

Authors: Kazuhisa Nakasho, Yasunari Shidama

Abstract: The purpose of this project is to collect symbol information in the Mizar Mathematical Library and manipulate it into practical and organized documentation. Inspired by the MathWiki project and API reference systems for computer programs, we developed a documentation generator focusing on symbols for the HTML-ized Mizar library. The system has several helpful features, including a symbol list, inc… ▽ More The purpose of this project is to collect symbol information in the Mizar Mathematical Library and manipulate it into practical and organized documentation. Inspired by the MathWiki project and API reference systems for computer programs, we developed a documentation generator focusing on symbols for the HTML-ized Mizar library. The system has several helpful features, including a symbol list, incremental search, and a referrer list. It targets those who use proof assistance systems, the volume of whose libraries has been rapidly increasing year by year. △ Less

Submitted 7 May, 2015; originally announced May 2015.

Comments: 5 pages, 1 figures, Conference on Intelligent Computer Mathematics 2015 (CICM2015)

ACM Class: G.4