×

Why are modal logics so robustly decidable? (English) Zbl 0935.03029

Summary: Modal logics are widely used in a number of areas in computer science, in particular for the specification and verification of hardware and software systems, for knowledge representation, in databases, and in artificial intelligence. The most important reason for the successful applications of these logics is that they provide a good balance between expressive power and computational complexity. In “Why is modal logic so robustly decidable? [in: N. Immerman et al. (eds.), Descriptive complexity and finite models. Proc. DIMACS Workshop, 1996, DIMASCS Ser. Discrete Math. Theor. Comput. Sci. 31, 149-183 (1997; Zbl 0881.03012)], M. Y. Vardi addressed the question to identify the main reasons for the robust decidability properties of modal logics. In particular he stressed the importance of the tree model property, which permits the use of powerful automata-theoretic techniques. Here we discuss this question in the light of recent research on guarded fragments of first-order logic and fixed point logic.

MSC:

03B45 Modal logic (including the logic of norms)
03B25 Decidability of theories and sets of sentences
03B20 Subsystems of classical logic (including intuitionistic logic)

Citations:

Zbl 0881.03012