| 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
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2018: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 情報理論 / 形式化 / Coq / Coqtop / Proviola / Python / 定理証明 / 情報源符号化 / シャノン理論 / SSReflect / 自動翻訳 |
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
情報理論の著名な諸定理を論理的な隙間なしに解説する文書が作成されることは、情報理論の基礎理論を頑健たるものにするだけでなく、初学者が誤解なく自主学習できる文献を提供できる。論理的に隙間のない証明として、計算機向けに形式化された証明が存在する。しかしこれは、人間にとってのReadabilityが欠如している。
本研究の目標が達成されれば、隙間なくReadabilityのある証明が得られることになる。
|
