2007 Fiscal Year Annual Research Report
| Project/Area Number |
19700127
|
|---|
| Research Institution | Saitama University |
|---|
Principal Investigator |
後藤 祐一 Saitama University, 理工学研究科, 助教 (70400801)
|
|---|
| Keywords | 情報システム / 知識工学 / 自動発見 |
|---|
| Research Abstract |
自動定理発見とは、予め与えられた定理を自動的に証明することではなく、計算機を用いて新しい定理を自動的に発見することである。自動定理発見問題は、自動定理発見の一般的な方法を求めるという問題である。この自動定理発見問題に対して帰結演算を用いた自動定理発見の理論的基礎と方法が提案された。この方法の特徴は、推論の妥当性を基礎付ける論理体系とそれぞれの分野の定義や公理、定理、また、それら二つを入力として受け取り入力された論理体系に従いそれぞれの分野の公理や定理から新たな定理の導出を行う椎論プログラムを明確に分離した点にある。帰結演算を用いた自動定理発見法を実現するためには、実用的な推論プログラムが必要不可欠であるが、そのような推論プログラムはいまだ実現されていない。本研究では、申請者が研究・開発を行ってきた汎用前向き自動帰結演算システムEnCalの汎用性と処理速度を高め、帰結演算による自動定理発見法の中心的部品である実用的な推論プログラムとして使用し、帰結演算による自動定理発見法に基づいた汎用的な自動定理発見ツールを開発することを目的としている。
形式論理における統語論の観点からすると、ある論理体系は、論理式を構成する語彙、論理式の構成規則、公理、そして、推論規則を定めることにより定義することができる。EnCalは、論理式を構成ずる語彙と論理式の構成規則、そして推論規則をプログラムに組み込む形で持っており、利用者がこれらを自由に定義することはできない。このため、任意の論理体系や形式理論を扱えないという問題があった。そこで、本度は、EnCa1を論理式を構成する語彙、論理式の構成規則、公理、そして、推論規則を入力として自由に与えられるようにした汎用前向き推論エンジンFreeEnCalの提案をし、そのプロトタイプの開発を行った。
|
Research Products
(4 results)
