Modal Satisfiability via SMT Solving

Carlos Areces 1 Pascal Fontaine 2 Stephan Merz 2
1 FaMAF - Facultad de Matemática, Astronomía y Física [Cordoba]
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Modal logics extend classical propositional logic, and they are robustly decidable. Whereas most existing decision procedures for modal logics are based on tableau constructions, we propose a framework for obtaining decision procedures by adding instantiation rules to standard SAT and SMT solvers. Soundness, completeness, and termination of the procedures can be proved in a uniform and elementary way for the basic modal logic and some extensions.
Keywords : modal logic satisfiability decision procedure SAT SMT
Type de document :
Chapitre d'ouvrage
Software, Services, and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, 8950, Springer, pp.30-45, 2015, Lecture Notes in Computer Science, 〈10.1007/978-3-319-15545-6_5〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01127966
Contributeur : Stephan Merz <>
Soumis le : lundi 9 mars 2015 - 08:55:57
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : lundi 17 avril 2017 - 04:48:53

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Carlos Areces, Pascal Fontaine, Stephan Merz. Modal Satisfiability via SMT Solving. Software, Services, and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, 8950, Springer, pp.30-45, 2015, Lecture Notes in Computer Science, 〈10.1007/978-3-319-15545-6_5〉. 〈hal-01127966〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

286

Téléchargements de fichiers

100

Contact


archive-ouverte@inria.fr