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
MPII - Max-Planck-Institut für Informatik, 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
Document type :
Book sections
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download
https://hal.inria.fr/hal-01127966
Contributor : Stephan Merz <>
Submitted on : Monday, March 9, 2015 - 8:55:57 AM
Last modification on : Saturday, August 3, 2019 - 1:23:14 AM
Long-term archiving on : Monday, April 17, 2017 - 4:48:53 AM

File

main.pdf
Files produced by the author(s)

Identifiers

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

346

Files downloads

231

Contact


archive-ouverte@inria.fr