高階論理における単一化アルゴリズムと定理証明の機械化に関する研究

1990 Fiscal Year Annual Research Report

• Project/Area Number: 01580020
• Research Institution: Kyushu Institute of Technology
• Principal Investigator: 原尾 政輝 九州工業大学, 情報工学部, 教授 (00006272)
• Co-Investigator(Kenkyū-buntansha): 藤田 憲悦 九州工業大学, 情報工学部, 助手 (30228994)
• Keywords: 高階論理 / λー算法 / 単一化アルゴリズム / 定理証明 / 証明の機械化 / 論理型言語 / 類推 / 推論機構

Research Abstract

平成2年度は,次の具体的研究課題を設定して研究を行った.(1)型付ーλ論理に基づく高階論理型言語の安定化,(2)高階論理の証明系の機械化のための単一化アルゴリズムの開発,(3)知識処理のための高階推論機構の開発.
課題(1)については,多様な知識構造を記述可能であってかつ効率的処理が可能な知識表現言語のための言語を目標にした.言語は,1階述語のホ-ン節を拡張した構文で,高階変数の出現や階数に制限を与えたλー項に基づくλー高階言語とし,その理論的性質および実装に関する研究を行った.課題(2)については,高階項の単一化アルゴリズムを知識処理への応用の立場から考察した.一般に高階単一化は計算不能であるが,高階項の階数や出現に制約を置き,用法に工夫すれば決定可能なクラスが存在する事が分った.また,NPー完全な問題に属するクラスや高階単一化の計算の複雑さの諸性質が明らかになった.特に,2階の項よりなる言語のクラスについては,知識処理として有効な応用法が存在し,どの様に用いれば計算可能な範囲で有効に高階論理を応用できるかについても分ってきた.課題(3)については,類推の問題を選んで考察した.ある種の類推システムが,抽象的な一般化知識を2階の論理式で,対象知識を1階の論理式で与え,類推処理を高階単一化機構によって自然な形で安定化できることを示した.特に,類推に基づく自動定理証明システムを提案し,原理的にそれが可能であることを具体的に示した.
このように,高階論理は多様な知識表現が可能で証明系も自然で簡潔である.したがって,有望な知識処理や人工知能のための枠組みであると思われる.

Research Products

• [Publications] 原尾,岩沼: "高階ユニフィケ-ションにおける可解なクラスと計算の複雑さ" LAシンポシウム,京都大学数理解研講究録. No.731. 37-48 (1990)
• [Publications] 岩沼,原尾: "非再帰的な述語サ-カムスクリプションの一階論理式への等価変換" 人工知能学会論文誌. Vol.5 No.4. 462-470 (1990)
• [Publications] Harao: "Analogical Reasoning Based on Higher Order Unification" First International Conference on Algorithmic Learning Theory. Proceeding. 151-163 (1990)
• [Publications] K.Iwanuma,M.Harao,S.Noguchi: "Reconsideration of Pointwise Circumscription,Transformation of NonーRecursive Predicate Circumscription into FirstーOrder Sentences" International Conferecnce on Info.Japan. Proceeding. 351-356 (1990)
• [Publications] K.Fujita,A.Togashi,S.Noguchi: "A Canonical Translation from Higher Order Logic to Typed Lambda Calculus" 人工知能学会誌. Vol.5 No.6. 796-807 (1990)
• [Publications] 原尾,岩沼: "高階項マッチングアルゴリズムの計算複雑さについて" 日本ソフトウェア科学会論文誌. Vol.8 No.1. 41-53 (1991)