解集合プログラミングによる様相命題論理Kの充足可能性判定
書誌事項
- タイトル別名
-
- Satisfiability Testing of Propositional Modal Logic K with Answer Set Programming
説明
<p>様相命題論理の体系Kについて，与えられた論理式の充足可能性を判定する新しい手法を提案する．提案する手法はタブロー法に基づいており，解集合プログラミングを用いて実装されている．タブロー法に基づいた既存手法では，可能世界を最初にすべて生成してから充足可能性判定を行う方法か，可能世界を幅優先的に順次拡大しながら充足可能性判定を繰り返し行う方法が取られている．提案するシステムでは，これらの方法に加え，ヒューリスティック関数を用いて可能世界を順次拡大する手法を導入している．ヒューリスティック関数を用いることで，充足不能になりそうな可能世界から先に探索することが可能になり，判定手続きの高速化につながることが期待できる．本手法を標準的なベンチマーク問題を用いて評価したところ，論理式の長さをヒューリスティック関数に用いた場合に，既存手法よりも良い結果が得られる場合があることがわかった．また，既存手法ではSATソルバーが利用されているが，本手法では解集合プログラミングを利用することで，非常に簡潔に証明系を記述できている点にも特徴がある．</p>
収録刊行物
-
- 人工知能学会全国大会論文集
-
人工知能学会全国大会論文集 JSAI2020 (0), 2N5OS17b05-2N5OS17b05, 2020
一般社団法人 人工知能学会
- Tweet
キーワード
詳細情報 詳細情報について
-
- CRID
- 1390003825189404032
-
- NII論文ID
- 130007856950
-
- 本文言語コード
- ja
-
- データソース種別
-
- JaLC
- CiNii Articles
- KAKEN
-
- 抄録ライセンスフラグ
- 使用不可
