Satisfiability Testing of Propositional Modal Logic K with Answer Set Programming
Satisfiability Testing of Propositional Modal Logic K with Answer Set Programming
复制标题
用答案集编程命题模态逻辑K的可满足性检验
DOI：
10.11517/pjsai.jsai2020.0_2n5os17b05
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
井上克巳
中科院分区：
文献类型：
--
作者：
飯野有軌;田村直之;宋剛秀;番原睦則;井上克巳
様相命題論理の体系 K について, 与えられた論理式の充足可能性を判定する新しい手法を提案する. 提案する手法はタブロー法に基づいており, 解集合プログラミングを用いて実装されている. タブロー法に基づいた既存手法では, 可能世界を最初にすべて生成してから充足可能性判定を行う方法か, 可能世界を幅優先的に順次拡大しながら充足可能性判定を繰り返し行う方法が取られている. 提案するシステムでは, これらの方法に加え, ヒューリスティック関数を用いて可能世界を順次拡大する手法を導入している. ヒューリスティック関数を用いることで, 充足不能になりそうな可能世界から先に探索することが可能になり, 判定手続きの高速化につながることが期待できる. 本手法を標準的なベンチマーク問題を用いて評価したところ, 論理式の長さをヒューリスティック関数に用いた場合に, 既存手法よりも良い結果が得られる場合があることがわかった. また, 既存手法では SAT ソルバーが利用されているが, 本手法では解集合プログラミングを利用することで, 非常に簡潔に証明系を記述できている点にも特徴がある.