Modal Satisfiability via SMT Solving - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Chapitre D'ouvrage Année : 2015

Modal Satisfiability via SMT Solving

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (194.8 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01127966 , version 1 (09-03-2015)

Identifiants

Citer

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⟩
172 Consultations
155 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More