第一階述語論理の決定可能なサブクラスに対する同値制約を考慮した充足可能性判定(検証・理論, 組込技術とネットワークに関するワークショップ)

スポンサーリンク

概要

論文の詳細を見る
近年の大規模化, 複雑化した半導体回路の検証の効率化のために, 限量子を含まない等号付第一階述語論理の充足可能性判定を用いた形式的検証手法が提案されている.しかし, 限量子を含まない等号付第一階述語論理では, 関数記号や述語記号に特別な意味づけが行われないため, そのままでは意図した通りの結果が得られない事がある.本報告では, 同値制約と呼ぶ式の集合を与える事により, 関数や述語の性質を考慮して充足可能性判定を行うアルゴリズムを示す.また, このアルゴリズムを実装し, 実験した結果について報告する.
社団法人電子情報通信学会の論文
2005-03-11

著者

関連論文

もっと見る

スポンサーリンク