Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [7 references]  Display  Hide  Download
Contributor : Valentin Montmirail <>
Submitted on : Monday, August 26, 2019 - 5:48:16 PM
Last modification on : Thursday, August 29, 2019 - 1:20:33 AM
Long-term archiving on: : Friday, January 10, 2020 - 1:22:12 PM


Files produced by the author(s)


  • HAL Id : hal-02271405, version 1



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⟩



Record views


Files downloads