Examples of Formal Proofs about Data Compression

DOI

書誌事項

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

説明

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.

収録刊行物

  • IEICE Proceeding Series

    IEICE Proceeding Series 55 665-669, 2018-10-18

    The Institute of Electronics, Information and Communication Engineers

詳細情報 詳細情報について

  • CRID
    1390845702310313088
  • NII論文ID
    230000011142
  • DOI
    10.34385/proc.55.we-pm-1-3.1
  • ISSN
    21885079
  • 本文言語コード
    en
  • データソース種別
    • JaLC
    • CiNii Articles
  • 抄録ライセンスフラグ
    使用不可

問題の指摘

ページトップへ