|
現在論理型言語は人工知能用言語の基礎となっているが、その優れた性質を保ちながらより高機能にする方法として高階論理への拡張が考えられる。本研究はその観点から、高階論理型言語の定式化と単一化アルゴリズムおよび高階論理系における証明論について研究を行なった。具体的には次の1〜3の課題に取り組み、以下に述べる成果を得た。
1.型付-λ論理に基づく高階論理型言語の定式化:型論理に基づく言語を対象に、構文論、意味論を検討した。特に、ホ-ン節構文を持つ言語を定義し、その公理系や推論規則および証明論について考察した。その結果、メタな知識や推論、類推等の定式化の可能な言語とその完全かつ健全な証明系の理論的性質と問題点がかなり明らかになった。
2.高階論理の証明系の機械化のための理論的性質:高階理論にも、基本的には一階論理で用いられている導出原理と同じ様な原理が拡張成立する。しかし、問題は単一化アルゴリズムと推論規則を適用する場合に生じる非決定的操作に在る事が分った。また、2階論理の範囲に限り、高階述語の単一化がマッチング(一方向)になるように制限したり、制約導出等の工夫を行う事によってある程度証明の機械化が可能との結果を得ている。
3.高階λ-論理言語での単一化アルゴリズムの設計:高階項の単一化アルゴリズムは一般に決定不能問題のクラスに属する。しかし、項の階数や高階項の出現に制限を加えることによって、幾つかの単一化アルゴリズムが計算可能となるクラスが明らかになった。また、高階項の単一化が難しくなる原因が、射影規則、模倣規則の組み合わせによって複雑な項の判定問題に帰着されるためである事等が明らかになった。さらに、これらの結果から高階論理言語を計算可能な範囲で有効に応用するための有用な幾つかの知見を得た。
|
