書誌事項
- タイトル別名
-
- トウシキ リロン オ ホウ ト スル DPLL センイケイ ニ ツイテ
- On DPLL Transition Systems Modulo Equational Theories
この論文をさがす
説明
SMTソルバは,指定された述語理論の下で論理式の充足可能性判定を行うツールであり,配列,リスト,キューなどの多くの理論を法として,論理式の充足可能性判定を行うことができる.しかし,利用者自身が定義した理論を法とする論理式の充足可能性判定を行うのは容易ではない.なぜならば,その理論に対する決定手続きを合わせて与えることが必要であるためである.本稿では,等式理論を法とする充足可能性判定手続きを状態遷移系DPLL(R)として定式化し,その実装方式を提案する.DPLL(R)は,与えられた等式理論から項書換え系の完備化手続きを用いて決定手続きを自動的に生成し,充足可能性判定を行う.従って,利用者は等式集合を等式理論として与えるだけでよく,決定手続きを与えなくてよい.
収録刊行物
-
- 電子情報通信学会技術研究報告SS, ソフトウェアサイエンス
-
電子情報通信学会技術研究報告SS, ソフトウェアサイエンス 110 (227), 49-54, 2010-10
一般社団法人電子情報通信学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1050001338803494272
-
- NII論文ID
- 120005530807
- 110008106386
-
- NII書誌ID
- AA1123312X
-
- HANDLE
- 2237/21153
-
- NDL書誌ID
- 10882012
-
- ISSN
- 09135685
-
- 本文言語コード
- ja
-
- 資料種別
- journal article
-
- データソース種別
-
- IRDB
- NDL
- CiNii Articles
- KAKEN
