Automated Generation of No Logical Gap Readable Proof for Information Theory

2018 Fiscal Year Final Research Report

• Project/Area Number: 16K12391
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Theory of informatics
• Research Institution: Chiba University
• Principal Investigator: Hagiwara Manabu 千葉大学, 大学院理学研究院, 准教授 (80415728)
• Co-Investigator(Kenkyū-buntansha): 葛岡 成晃 和歌山大学, システム工学部, 准教授 (60452538)
• Research Collaborator: Garrigue Jacques ; Nakano Kyosuke ; Kong Justin
• Project Period (FY): 2016-04-01 – 2019-03-31
• Keywords: 情報理論 / 形式化

Outline of Final Research Achievements

As an application of the library InfoTheo on Coq / MathComp for information theory, we challenged the implementation of software that converts .v files of the library into human readable natural language. The approach is based on customization of the software Proviolla and creating completely original source code on Python, and replacing MathComp tactics and Coq commands with human readable natural language.

Free Research Field

符号理論

Academic Significance and Societal Importance of the Research Achievements

情報理論の著名な諸定理を論理的な隙間なしに解説する文書が作成されることは、情報理論の基礎理論を頑健たるものにするだけでなく、初学者が誤解なく自主学習できる文献を提供できる。論理的に隙間のない証明として、計算機向けに形式化された証明が存在する。しかしこれは、人間にとってのReadabilityが欠如している。
本研究の目標が達成されれば、隙間なくReadabilityのある証明が得られることになる。