| 研究課題/領域番号 |
16K12391
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
萩原 学 千葉大学, 大学院理学研究院, 准教授 (80415728)
|
|---|
| 研究分担者 |
葛岡 成晃 和歌山大学, システム工学部, 准教授 (60452538)
|
|---|
| 研究協力者 |
ガリグ ジャック
中野 恭輔
コング ジャスティン
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| 研究課題ステータス |
完了 (2018年度)
|
| 配分額 *注記 |
3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2018年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2017年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2016年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | 情報理論 / 形式化 / Coq / Coqtop / Proviola / Python / 定理証明 / 情報源符号化 / シャノン理論 / SSReflect / 自動翻訳 |
|---|
| 研究成果の概要 |
Coq/MathComp上の情報理論ライブラリInfoTheoの活用として、そのライブラリの.vファイルを人間が読解可能な文章へ変換するソフトウェアの実装に挑戦した。アプローチはソフトウェアProviollaをベースとしつつ、Pythonベースの完全オリジナルソースコードを作成し、MathCompのタクティクやCoqのコマンドを自然言語へ置き換えるものである。
|
| 研究成果の学術的意義や社会的意義 |
情報理論の著名な諸定理を論理的な隙間なしに解説する文書が作成されることは、情報理論の基礎理論を頑健たるものにするだけでなく、初学者が誤解なく自主学習できる文献を提供できる。論理的に隙間のない証明として、計算機向けに形式化された証明が存在する。しかしこれは、人間にとってのReadabilityが欠如している。
本研究の目標が達成されれば、隙間なくReadabilityのある証明が得られることになる。
|
