| 研究課題/領域番号 |
15H06081
|
|---|
| 研究機関 | 埼玉大学 |
|---|
研究代表者 |
高 宏彪 埼玉大学, 理工学研究科, 助教 (50756955)
|
|---|
| 研究期間 (年度) |
2015-08-28 – 2017-03-31
|
| キーワード | 自動推論 / 自動定理発見 / 認識的プログラミング / 離散数学 |
|---|
| 研究実績の概要 |
1988年Wosにより提案された世界的に知られている未解決難問である自動定理発見問題とは、新しくて面白い定理を自動的に発見する自動推論プログラムが持つべき一般的性質を明らかにする問題である。その解決は、様々な分野で多くの応用があり、特に、計算的学習、予測、発見に対して系統的な方法論と強力的な道具を提供することができる。本研究は、応募者が既に提案した自動定理発見のための系統的方法論に基づいて、認識的プログラミングによる自動定理発見を行うという新しい試みで、科学者の学習、予測、発見における認識プロセスに対して、認識的プログラミングパラダイムの有効性と実用性を明らかにする。
平成２７年度では、まず、強相関論理EcQの第2級（論理定理における必然的帰結演算子の入れ子の深さは2まで）論理定理集合に基づいて、汎用前向き推論エンジンFreeEnCalを用いてNBG公理集合論、初等整数論、公理幾何学の第2級形式理論の定理集合を生成した。また、強相関論理EcQの第2級論理定理集合および上記得たNBG公理集合論の第2級形式理論に基づいて、FreeEnCalを用いてグラフ理論の第2級形式理論を生成した。そして、生成したNBG集合論、初等整数論、グラフ理論、公理幾何学の第2級形式理論を分析し、新しく面白い定理の四つの影響要素を見つけ、それらの影響要素に基づいて、定理の面白さの計量(metric)を提案した。さらに、上記の研究を踏まえ、EPLASを用いて、前向き演繹、新しい経験定理の候補として列挙し、述語抽象、帰納推論などの自動定理発見の各プロセスを記述した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
当初計画では、強相関論理EcQの第３級論理定理集合に基づいて、FreeEnCalを用いて、NBG集合論の第３級形式理論を生成するつもりですが、実験用サーバのメモリ（32GB）で導出できなかった。現時点では、強相関論理EcQの第2級論理定理集合に基づいて、FreeEnCalを用いて、NBG公理集合論の第2級形式理論を生成した。
|
| 今後の研究の推進方策 |
まず、FreeEnCalのアルゴリズムを改善し、いまの実験用サーバで強相関論理EcQの第３級論理定理集合を生成する予定です。そして、強相関論理EcQの第３級論理定理集合に基づいて、FreeEnCalを用いて、NBG集合論、初等整数論、グラフ理論、組合せ理論、抽象代数学、公理幾何学の第３級形式理論を生成する。また、NBG集合論、初等整数論、グラフ理論、組合せ理論、抽象代数学、公理幾何学の既知定理および既知未解決問題も強相関論理EcQに基づいて形式化し、それらを合わせてNBG集合論、初等整数論、グラフ理論、組合せ理論、抽象代数学、公理幾何学の形式理論知識ベースをそれぞれ構築し、認識的プログラミングによる定理発見を試みる。最後、認識的プログラミングによる定理発見の実験結果を確認し、認識的プログラミングパラダイムの有効性と実用性を明らかにする。
|
