2008 Fiscal Year Annual Research Report
| Project/Area Number |
19700127
|
|---|
| Research Institution | Saitama University |
|---|
Principal Investigator |
後藤 祐一 Saitama University, 理工学研究科, 助教 (70400801)
|
|---|
| Keywords | 情報システム / 知識工学 / 自動発見 |
|---|
| Research Abstract |
自動定理発見とは、予め与えられた定理を自動的に証明することではなく、計算機を用いて新しい定理を自動的に発見することである。自動定理発見問題は、自動定理発見の一般的な方法を求めるという問題である。この自動定理発見問題に対して帰結演算を用いた自動定理発見の理論的基礎と方法が提案された。この方法の特徴は、推論の妥当性を基礎付ける論理体系とそれぞれの分野の定義や公理、定理、また、それら二つを入力として受け取り入力された論理体系に従いそれぞれの分野の公理や定理から新たな定理の導出を行う推論プログラムを明確に分離した点にある。帰結演算を用いた自動定理発見法を実現するためには、実用的な推論プログラムが必要不可欠であるが、そのような推論プログラムはいまだ実現されていない。本研究では、帰結演算による自動定理発見法に基づいた汎用的な自動定理発見ツールを開発することを目的としている。平成19年度は論理式を構成する語彙、論理式の構成規則、公理、そして、推論規則を入力として自由に与えられるようにした汎用前向き推論エンジンFreeEnCalのプロトタイプの開発を行った。
本年度は、平成19年度に開発したFreeEnCalの処理アルゴリズムを見直し処理の高速化を試みた。FreeEnCalの処理時間の大半は導出された結論が既に導出済みであるかどうかを調べる重複検査処理に費やされていた。そこで、FreeEnCalの処理対象である論理式の構造に着目し、重複検査を論理式単位ではなく、論理式を構成する要素単位で行い、無駄な処理を削減することによって処理の高速化を行った。これにより、従来の重複検査アルゴリズムに比べて大幅な速度向上を達成することができた。
|
