No label defined (Q4353561)

In order to present an all-inclusive and convincing answer to the question raised in the title of the paper, in its first part the author considers the relationships of propositional modal logic and first-order logic; in the second part of the paper the connections between modal logic and computation-tree logic [see \textit{E. M. Clarke} and \textit{E. A. Emerson}, Lect. Notes Comput. Sci. 131, 52-71 (1982; Zbl 0546.68014)] are treated. Namely, the fact that modal logic can be viewed as a fragment of two-variable first-order logic provides some explanation for the tractability of modal logic, but not a quite satisfactory one. On the other hand, the decidability of computation-tree logic, which is an extension of modal logic, can be explained by the so-called tree-model property. It is shown how the tree-model property, enjoyed by modal logic and its extensions, leads to automata-based decision procedures. For the entire collection see [Zbl 0865.00055].