Satisfiability Testing of Propositional Modal Logic K with Answer Set Programming

DOI Open Access

Bibliographic Information

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

Description

<p>In this paper, we propose a new method for testing satisfiability of the given formula in propositional modal logic K. The proposed way is based on a tableau method and implemented in answer set programming. In previous tableau based solvers, such as Km2SAT and InKreSAT, the satisfiability is tested after creating all possible worlds initially, or it is tested repeatedly by incrementally extending the possible worlds with a breadth-first strategy. The proposal introduces a new way to extend the possible worlds incrementally with a heuristic function in addition to these two previous methods. By using appropriate heuristics, it is expected to search an unsatisfiable possible world first, and will improve the testing performance. We evaluated the proposed method with a standard benchmark set LWB and found the proposal was superior to the existing methods in some benchmark class when the length of the given formula is used as the heuristic function.</p>

Journal

Related Projects

See more

Keywords

Details 詳細情報について

  • CRID
    1390003825189404032
  • NII Article ID
    130007856950
  • DOI
    10.11517/pjsai.jsai2020.0_2n5os17b05
  • ISSN
    27587347
  • Text Lang
    ja
  • Article Type
    journal article
  • Data Source
    • JaLC
    • CiNii Articles
    • KAKEN
  • Abstract License Flag
    Disallowed

Report a problem

Back to top