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 詳細情報について

Report a problem

Back to top