| HAL-Inria | Publications, software ... of Inria's scientists |
Book sections
Modal Satisfiability via SMT Solving
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.
Cited literature [25 references]
https://hal.inria.fr/hal-01127966
Contributor : Stephan Merz <>
Submitted on : Monday, March 9, 2015 - 8:55:57 AM
Last modification on : Tuesday, December 8, 2020 - 10:19:47 AM
Long-term archiving on: : Monday, April 17, 2017 - 4:48:53 AM
Contributor : Stephan Merz <>
Submitted on : Monday, March 9, 2015 - 8:55:57 AM
Last modification on : Tuesday, December 8, 2020 - 10:19:47 AM
Long-term archiving on: : Monday, April 17, 2017 - 4:48:53 AM
File
main.pdf
Files produced by the author(s)