2016 Fiscal Year Annual Research Report
Automated Theorem Finding by Epistemic Programming
| Project/Area Number |
15H06081
|
|---|
| Research Institution | Saitama University |
|---|
Principal Investigator |
高 宏彪 埼玉大学, 理工学研究科, 助教 (50756955)
|
|---|
| Project Period (FY) |
2015-08-28 – 2017-03-31
|
| Keywords | 自動推論 / 自動定理発見 / 認識的プログラミング / 離散数学 |
|---|
| Outline of Annual Research Achievements |
1988年Wosにより提案された世界的に知られている未解決難問である自動定理発見問題とは、新しくて面白い定理を自動的に発見する自動推論プログラムが持つべき一般的性質を明らかにする問題である。その解決は、様々な分野で多くの応用があり、特に、計算的学習、予測、発見に対して系統的な方法論と強力的な道具を提供することができる。本研究は、応募者が既に提案した自動定理発見のための系統的方法論に基づいて、認識的プログラミングによる自動定理発見を行うという新しい試みで、科学者の学習、予測、発見における認識プロセスに対して、認識的プログラミングパラダイムの有効性と実用性を明らかにする。
今年度では、前年度に生成したNBG集合論、初等整数論、グラフ理論、公理幾何学の第2級形式理論を分析し、更に959個初等整数論の既知な定理の面白さの影響要素を調査し、汎用な定理の面白さの計量(metric)を定義した。そして、導出したNBG集合論、初等整数論の第2級形式理論の経験定理の面白さを定義した汎用な定理の面白さの計量を使って、実際に計量した。計量した結果、予期しなかった定理の面白さの数値が正規分布に近づくという結果が判明した。その結果を精査する必要があるため、平成２９年度まで繰越した。平成２９年度では、定理の面白さの数値の分布の結果を精査し、さらにNBG集合論と初等整数論の計量した結果を比較し、二つの分野の導出した定理が似ている面白さの数値の分布を持つという結果を国際会議に公表した。また、離散数学における概念の学習と発見だけでなく、暗号プロトコルの推論的分析による欠陥発見、新しい攻撃パターンの予測と発見、などの事例研究を行って、事例研究の結果はこの研究の実用性を示した。
|
| Research Progress Status |
28年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
28年度が最終年度であるため、記入しない。
|
Research Products
(5 results)
