View article

This paper is a survey and systematic presentation of decidability and complexity issues for modal and non-modal two-variable logics. A classical result due to Mortimer says that the two-variable fragment of first-order logic, denoted FO², has the finite model property and is therefore decidable for satisfiability. One of the reasons for the significance of this result is that many propositional modal logics can be embedded into FO². Logics that are of interest for knowledge representation, for the specification and verification of concurrent systems and for other areas of computer science are often defined (or can be viewed) as extensions of modal logics by features like counting constructs, path quantifiers, transitive closure operators, least and greatest fixed points, etc. Examples of such logics are computation tree logic CTL, the modal μ-calculus L_μ, or popular description logics used in artificial intelligence. Although the …