解集合プログラミングによる様相命題論理Kの充足可能性判定

DOI オープンアクセス

書誌事項

タイトル別名
  • Satisfiability Testing of Propositional Modal Logic K with Answer Set Programming

抄録

<p>様相命題論理の体系Kについて,与えられた論理式の充足可能性を判定する新しい手法を提案する.提案する手法はタブロー法に基づいており,解集合プログラミングを用いて実装されている.タブロー法に基づいた既存手法では,可能世界を最初にすべて生成してから充足可能性判定を行う方法か,可能世界を幅優先的に順次拡大しながら充足可能性判定を繰り返し行う方法が取られている.提案するシステムでは,これらの方法に加え,ヒューリスティック関数を用いて可能世界を順次拡大する手法を導入している.ヒューリスティック関数を用いることで,充足不能になりそうな可能世界から先に探索することが可能になり,判定手続きの高速化につながることが期待できる.本手法を標準的なベンチマーク問題を用いて評価したところ,論理式の長さをヒューリスティック関数に用いた場合に,既存手法よりも良い結果が得られる場合があることがわかった.また,既存手法ではSATソルバーが利用されているが,本手法では解集合プログラミングを利用することで,非常に簡潔に証明系を記述できている点にも特徴がある.</p>

収録刊行物

関連プロジェクト

もっと見る

詳細情報 詳細情報について

  • CRID
    1390003825189404032
  • NII論文ID
    130007856950
  • DOI
    10.11517/pjsai.jsai2020.0_2n5os17b05
  • 本文言語コード
    ja
  • データソース種別
    • JaLC
    • CiNii Articles
    • KAKEN
  • 抄録ライセンスフラグ
    使用不可

問題の指摘

ページトップへ