Skip to Main content Skip to Navigation
Book sections

Modal Satisfiability via SMT Solving

Carlos Areces 1 Pascal Fontaine 2 Stephan Merz 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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.
Document type :
Book sections
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Monday, March 9, 2015 - 8:55:57 AM
Last modification on : Saturday, October 16, 2021 - 11:26:05 AM
Long-term archiving on: : Monday, April 17, 2017 - 4:48:53 AM


Files produced by the author(s)




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⟩



Les métriques sont temporairement indisponibles