Examples of Formal Proofs about Data Compression

DOI

Bibliographic Information

Published
2018-10-18
DOI
  • 10.34385/proc.55.we-pm-1-3.1
Publisher
The Institute of Electronics, Information and Communication Engineers

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

Details 詳細情報について

  • CRID
    1390845702310313088
  • NII Article ID
    230000011142
  • DOI
    10.34385/proc.55.we-pm-1-3.1
  • ISSN
    21885079
  • Text Lang
    en
  • Data Source
    • JaLC
    • CiNii Articles
  • Abstract License Flag
    Disallowed

Report a problem

Back to top