On Checking Kripke Models for Modal Logic K - Université Côte d'Azur Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

On Checking Kripke Models for Modal Logic K

Résumé

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
Origine Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

  • HAL Id : hal-02271413 , version 1

Citer

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 Consultations
125 Téléchargements

Partager

Gmail Mastodon Facebook X LinkedIn More