Presentation information

Organized Session

Organized Session » OS-17

[2N5-OS-17b] OS-17 (2)

Wed. Jun 10, 2020 3:50 PM - 5:30 PM Room N (jsai2020online-14)

宋 剛秀(神戸大学)、沖本 天太(神戸大学)

5:10 PM - 5:30 PM

[2N5-OS-17b-05] Satisfiability Testing of Propositional Modal Logic K with Answer Set Programming

Naoki Iino1, 〇Naoyuki Tamura1, Takehide Soh1, Mutsunori Banbara2, Katsumi Inoue3 (1. Kobe University, 2. Nagoya University, 3. National Institute of Informatics)

Keywords:Propositional Modal Logic, Answer Set Programming, Satisfiability Testing

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.

Authentication for paper PDF access

A password is required to view paper PDFs. If you are a registered participant, please log on the site from Participant Log In.
You could view the PDF with entering the PDF viewing password bellow.