ATMSと単純化順序を用いた項書き換えシステム停止性検証システムの開発 : 第2報

概要

論文の詳細を見る
項書き換えシステム(Term Rewriting System:TRS)はl→rの形をした書き換え規則(rewrit rule)の集合として記述されたプログラムである。ここでl,rは変数、演算子から構成された項である(rに含まれる変数はlにも含まれる)。一般にTRSの停止性を検証することは決定不能な問題であることが知られているが、単純化順序[1]を用いることによって与えられた特定のクラスのTRSの停止性を検証することが可能である。本稿では単純化順序として辞書武経路順序を用いるが、辞書試経路順序を用いるためには項を構成している演算子の集合上の半順序を≻決定しなければならない。この決定問題は通常のバックトラック法を用いることによって決定することが可能であるが、多くの無駄なバックトラック、推論の再検知、矛盾の再検知を行なう。筆者らは[6,7]においてこれらの問麺急を解決するためATM[3]の利用を提案した。本稿では、さらにこのATMSを拡張し、新しいnogoodの計算のためにhyperresolutionの利用を示す。また、justificationの計算など、ATMS利用のためのプロトコルを明確にする。
一般社団法人情報処理学会の論文
1990-09-04