On logics with two variables
type: Item
instance of: scholarly article
title: On logics with two variables
zbMATH Open document ID: 0948.03023
DOI: 10.1016/S0304-3975(98)00308-9
author: Erich Grädel
author: Martin Otto
published in: Theoretical Computer Science
publication date: 2000-01-12T00:00:00Z
review text: 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 \(\text{FO}^{2}\), 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 \(\text{FO}^{2}\). 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 \(\mu\)-calculus \(L_{\mu}\), or popular description logics used in artificial intelligence. Although the additional features are usually not first-order constructs, the resulting logics can still be seen as two-variable logics that are embedded in suitable extensions of \(\text{FO}^{2}\). Typically, the applications call for an analysis of the satisfiability and model checking problems of the logics employed. The decidability and complexity issues for modal and non-modal two-variables logics have been studied quite intensively in the last years. It has turned out that the satisfiability problems for two-variable logics with full first-order quantification are usually much harder (and indeed highly undecidable in many cases) than the satisfiability problems for corresponding modal logics. On the other hand, the situation is different for model checking problems. The model checking problem of a modal logic has essentially the same complexity as the model checking problem of the corresponding two-variable logic with full quantification.
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 1387346
zbMATH Keywords: two-variable logics
zbMATH Keywords: modal logics
zbMATH Keywords: satisfiability
zbMATH Keywords: model checking
zbMATH Keywords: survey
zbMATH Keywords: decidability
zbMATH Keywords: complexity
reviewed by: Damas Gruska
MaRDI profile type: Publication
cites work: Q3996675
cites work: Q3122692
cites work: The undecidability of the domino problem
cites work: Q5691140
cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications
cites work: Q4362912
cites work: On model checking for the \(\mu\)-calculus and its fragments
cites work: Q3341896
cites work: On the Restraining Power of Guards
cites work: On the Decision Problem for Two-Variable First-Order Logic
cites work: Undecidability results on two-variable logics
cites work: Q3903002
cites work: Remarks on Berger's paper on the domino problem
cites work: Q3995676
cites work: Q4003410
cites work: Q4936118
cites work: A finite model theorem for the propositional \(\mu\)-calculus
cites work: Complexity results for classes of quantificational formulas
cites work: On languages with two variables
cites work: A calculus of communicating systems
cites work: Q4376070
cites work: Bounded variable logics: Two, three, and more
cites work: Q4298260
cites work: Undecidable theories
cites work: Q4353561
description: scientific article; zbMATH DE number 1387346