Modal Satisfiability via {SMT} Solving

TitleModal Satisfiability via {SMT} Solving
Publication TypeBook Chapter
Year of Publication2015
AuthorsAreces, C, Fontaine, P, Merz, S
EditorDe Nicola, R, Hennicker, R
Book TitleSoftware, Services, and Systems
Series TitleLecture Notes in Computer Science
Volume8950
Pagination30-45
PublisherSpringer International Publishing
ISBN Number978-3-319-15544-9
AbstractModal 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.
URLhttp://dx.doi.org/10.1007/978-3-319-15545-6_5
DOI10.1007/978-3-319-15545-6_5
Work Package: 
WP2