ビット列を用いた節集合のリネーミング法

概要

論文の詳細を見る
従来,節集合をHorn節集合に変換するリネーミングは発見的手法を用いて求められてきた.近年,西岡^<(5)〜(8)>により0-1計画法等を用いたリネーミング法が考案されている.これらの方法は系統的にリネーミングを行う方法を示しているが,そのためには,0-1計画法や行列演算等の複雑なアルゴリズムを必要としていた.本論文では節集合に含まれる各述語に対応するビット列を定義し,これを用いてビット列演算を行うことにより,その演算結果から節集合をHorn節集合に変換するすべてのリネーミングが導かれることを証明する.本方法は従来のリネーミング法と異なり,すべてのリネーミングを並行して一度に求めることのできる効率の良い計算法となっている.また,本方法はビット列間の並列ビット演算の組合せのみでリネーミングが計算できるため,特別な処理システムを必要とせず,ビット列に対する演算を行えるプログラミング言語ならどれを用いても計算を行える利点がある.更に,リネーミングを求めるのに必要とされる演算回数を容易に求められるのも本方法の特長である.
社団法人電子情報通信学会の論文
1993-11-25