1992 Fiscal Year Annual Research Report
型理論に基づく高階推論機構の形式化とその類推処理への応用
| Project/Area Number |
04650320
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
原尾 政輝 九州工業大学, 情報工学部, 教授 (00006272)
|
|---|
| Keywords | 型理論 / 高階論理 / 推論機構 / 類推 / 知識ベース / 自然演繹証明 / ML |
|---|
| Research Abstract |
平成4年度は次の具体的課題を設定して研究を進めてきた.(1)型理論に基づく高階計算言語の設計と推論機構の研究,(2)抽象化に基づく類推システムの形式化,(3)高階論理の定理証明系の機械化.
まず(1)の課題に対しては,単純型理論に基づく高階論理言語をホーン節の拡張である高階ホーン節構文で設計し,関数型言語であるMLを用いて実現した.その処理系は,自然演繹法に基づく高階推論機構を用いて構成されており,現在高階マッチングの処理に少し問題があるが,高階論理言語としての大体の機能を実現することが出来た.また,高階論理言語を用いた,知識ベース,推論,を始めとする知能ソフトウェアの作成への応用を試みている.
次の(2)の課題については,対象をLK定理証明システムとして採り,問題間の類似性を援用して証明する類推システムを言語Isabelleを用いて実装した.システムの基本機能としては,問題の類似性を検出しスキーマ(2階の論理式)として一般化しスキーマベースを構成する過程,与えられた問題に対して適用可能なスキーマを検索し証明情報を計算する過程,証明情報から具体的証明を作り出す過程,からなる.現在,30程度のスキーマよりなるシステムとなっており,大学の初級程度の証明能力を備えている.
(3)の課題については,自然演繹証明の良さを全面に出した高階証明方式を設計する立場から,新しく展開木とLK証明システムを融合した方式について研究を進めた.その方式を言語Isabelleを用いて一部実現した.
|
-
[Publications] 原尾 政輝: "高階一般化による類推" 人工知能研究会資料,人工知能基礎論. 75-14. 127-136 (1991)
-
[Publications] 中川 祥子,原尾 政輝: "類推によるLK定理証明" 電子情報通信学会,コンピュテーション研究会資料. COMP92-36. 63-70 (1992)
-
[Publications] M.Harao: "Analogical Reasoning For Natural Deduction Theorem Proving," 自動推論に関する国際ワークショップ(Int.Workshop on Automated Reasoning). 220-228 (1992)
-
[Publications] M.Harao: "LK Theorem Proving By Analogy" 環太平洋人工知能国際会議(PRICAI'92). 714-720 (1992)
