On Checking Kripke Models for Modal Logic K - Université Côte d'Azur Access content directly
Conference Papers Year : 2016

On Checking Kripke Models for Modal Logic K


This article presents our work toward a rigorous experimental comparison of state-of-the-art solvers for the resolution of the satisfiability of formulae in modal logic K. Our aim is to provide a pragmatic way to verify the answers provided by those solvers. For this purpose, we propose a certificate format and a checker to validate Kripke models for modal logic K. We present some experimental results using efficient solvers modified to incorporate this verification step. We have been able to validate at least one certificate for 67 percent of the satisfi-able problems, which provides a set of benchmark with independently checked solution which can be used to validate new solvers. We discuss the limits of our approach in the last part of this article.
Fichier principal
Vignette du fichier
paper-07.pdf (1.93 Mo) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

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


  • HAL Id : hal-02271413 , version 1


Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail. On Checking Kripke Models for Modal Logic K. Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, July 2nd, 2016., Jul 2016, Coimbra, Portugal. ⟨hal-02271413⟩
63 View
124 Download


Gmail Mastodon Facebook X LinkedIn More