Modal Satisfiability via {SMT} Solving
| Title | Modal Satisfiability via {SMT} Solving |
| Publication Type | Book Chapter |
| Year of Publication | 2015 |
| Authors | Areces, C, Fontaine, P, Merz, S |
| Editor | De Nicola, R, Hennicker, R |
| Book Title | Software, Services, and Systems |
| Series Title | Lecture Notes in Computer Science |
| Volume | 8950 |
| Pagination | 30-45 |
| Publisher | Springer International Publishing |
| ISBN Number | 978-3-319-15544-9 |
| 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. |
| URL | http://dx.doi.org/10.1007/978-3-319-15545-6_5 |
| DOI | 10.1007/978-3-319-15545-6_5 |
Work Package:
WP2
