ステータス付き再帰的経路順序による項書換え系多重完備化手続きの実装と性能評価

佐藤 晴彦  栗原 正仁  

誌名
電子情報通信学会論文誌 D   Vol.J89-D   No.4   pp.624-631
発行日: 2006/04/01
Online ISSN: 1881-0225
Print ISSN: 1880-4535
論文種別: 特集論文 (フォーマルアプローチ論文特集)
専門分野: 計算モデル
キーワード: 
項書換え系,  ステータス付き再帰的経路順序,  多重完備化手続き,  BDD,  

本文: PDF(406.7KB)
>>論文を購入


あらまし: 
本論文では,多重完備化手続きMKBpoにおいて取り扱う簡約順序を辞書式経路順序(LPO)としたMKBlpoからステータスを用いた再帰的経路順序(RPOS)に拡張することで,完備化が可能となる範囲を大きく広げた完備化手続きMKBrposの実装とその性能評価について報告する.MKBlpo と同様,RPOSの集合を論理関数で表現し,BDDで処理することにより高速化を図っている.実験により,考慮すべき順序の数が多い場合は,考え得るすべてのRPOSをMKBで並列に取り扱った場合よりも高速であることを示す.また,MKBlpoで解ける問題についても,考慮すべきステータスの組合せが数倍から数百倍多いにもかかわらず,平均的にわずかな計算時間のオーバヘッドで解くことができることを実証する.