- 【Updated on January 20, 2026】 Integration of CiNii Books into CiNii Research
- Trial version of CiNii Research Knowledge Graph Search feature is available on CiNii Labs
- 【Updated on November 26, 2025】Regarding the recording of “Research Data” and “Evidence Data”
- CiNii Research researchers search function has been released.
Examples of Formal Proofs about Data Compression
-
- Reynald Affeldt
- National Institute of Advanced Industrial Science and Technology
-
- Jacques Garrigue
- Nagoya University
-
- Takafumi Saikawa
- Nagoya University
Description
Because of the increasing complexity of mathematical proofs, there is a growing interest in formalization using proof-assistants. In this paper, we explain new formal proofs of standard lemmas in data compression (Jensen’s and Kraft’s inequalities) as well as concrete applications (to the analysis of compression methods and Shannon-Fano codes). We explain in particular how one turns the paper proof into formal terms and the relation between the informal proof and the formal one. These formalizations come as an extension to an existing formal library for information theory and error-correcting codes.
Journal
-
- IEICE Proceeding Series
-
IEICE Proceeding Series 55 665-669, 2018-10-18
The Institute of Electronics, Information and Communication Engineers
- Tweet
Details 詳細情報について
-
- CRID
- 1390845702310313088
-
- NII Article ID
- 230000011142
-
- ISSN
- 21885079
-
- Text Lang
- en
-
- Data Source
-
- JaLC
- CiNii Articles
-
- Abstract License Flag
- Disallowed