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