Elementary Modal Logics over Transitive Structures

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.

Authors

• Jakub Michaliszyn
• Jan Otop

Keywords

• Modal logic
• Transitive frames
• Elementary modal logics
• Decidability