基底ナローイングを用いた拡張単一化アルゴリズムの完全性問題
スポンサーリンク
概要
- 論文の詳細を見る
基底ナローイングによる拡張単一化とは,項書換えシステムが与えられたとき,2つの項を等しくするような代入を求める手続きである.そのアルゴリズムは,SLD反駁との対応を利用して効率化されている.しかし,その完全性定理の証明には反例が存在する.本稿では,基底ナローイングと最内リダクションの関係を明らかにし,基底ナローイングによる拡張単一化の完全性を証明する.さらに,基底ナローイングの切換え補題を与え,効率化されたアルゴリズムについても完全性を証明する.
- 1989-07-14