LIPIcs.CSL.2013.563.pdf
- Filesize: 444 kB
- 15 pages
We show that modal logic over universally first-order definable classes of transitive frames is decidable. More precisely, let K be an arbitrary class of transitive Kripke frames definable by a universal first-order sentence. We show that the global and finite global satisfiability problems of modal logic over K are decidable in NP, regardless of choice of K. We also show that the local satisfiability and the finite local satisfiability problems of modal logic over K are decidable in NExpTime.
Feedback for Dagstuhl Publishing