著者

原尾 政輝 岩沼 宏治

出版者

一般社団法人日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.8, no.1, pp.41-53, 1991-01-14

被引用文献数

6

---

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