A SAT-Based Approach For PSPACE Modal Logics

Abstract : SAT solvers have become efficient for solving NP-complete problems (and beyond). Usually those problems are solved by direct translation to SAT or by solving iteratively SAT problems in a procedure like CEGAR. Recently, a new recur-sive CEGAR loop working with two abstraction levels, called RECAR, was proposed and instantiated for modal logic K. We aim to complete this work for modal logics based on axioms (B), (D), (T), (4) and (5). Experimental results show that the approach is competitive against state-of-the-art solvers for modal logics K, KT and S4.
Document type :
Conference papers
Complete list of metadatas

Cited literature [7 references]  Display  Hide  Download

https://hal.univ-cotedazur.fr/hal-02271405
Contributor : Valentin Montmirail <>
Submitted on : Monday, August 26, 2019 - 5:48:16 PM
Last modification on : Thursday, August 29, 2019 - 1:20:33 AM

File

KR.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02271405, version 1

Collections

Citation

Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail. A SAT-Based Approach For PSPACE Modal Logics. Principles of Knowledge Representation and Reasoning: Sixteenth International Conference, Oct 2018, Tempe, United States. ⟨hal-02271405⟩

Share

Metrics

Record views

9

Files downloads

7