A SAT-Based Approach For PSPACE Modal Logics - Université Côte d'Azur Access content directly
Conference Papers Year : 2018

A SAT-Based Approach For PSPACE Modal Logics


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.
Fichier principal
Vignette du fichier
KR.pdf (381.38 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-02271405 , version 1 (26-08-2019)


  • 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⟩
62 View
95 Download


Gmail Mastodon Facebook X LinkedIn More