高階ユニフィケーションアルゴリズムの複雑さについて (<特集>関数型プログラミングと計算の基礎)

スポンサーリンク

概要

論文の詳細を見る
ある言語におけるユニフィケーション問題とは,その言語の任意の項t_1,t_2が与えられたとき,σ(t_1)=σ(t_2)となる置換(ユニファイア)σが存在するか判定する問題である.ユニフィケーションは,定理証明の機械化や記号処理等と関連して重要である.本稿では,高階論理における項のユニフィケーションについてアルゴリズム論的立場から考察する.一般に,2階以上の項のユニフィケーション問題は決定不能であるが,いくつかの制限付き導出規則の下でユニフィケーション問題が可解となることを示す.また,実用上有用な2階のクラスについて,計算の複雑さがNP-完全となるものが存在することを示す.
一般社団法人日本ソフトウェア科学会の論文
1991-01-14

著者

関連論文

もっと見る

スポンサーリンク