Modal Satisfiability via SMT Solving

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.
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 : mercredi 8 novembre 2017 - 12:08:09
Document(s) archivé(s) le : lundi 17 avril 2017 - 04:48:53

Fichier

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

Identifiants

Collections

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〉

Partager

Métriques

Consultations de la notice

228

Téléchargements de fichiers

84