On logics with two variables

DOI10.1016/S0304-3975(98)00308-9zbMath0948.03023MaRDI QIDQ1960419

Martin Otto, Erich Grädel

Publication date: 12 January 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

surveycomplexitydecidabilitymodel checkingsatisfiabilitymodal logicstwo-variable logics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15)

Related Items

The guarded fragment with transitive guards, A logical approach to locality in pictures languages, Expressive power of ``now and ``then operators, Small substructures and decidability issues for first-order logic with two variables, Data-complexity of the two-variable fragment with counting quantifiers, Communicating Finite-State Machines and Two-Variable Logic, Graphs Identified by Logics with Counting, A Decidable Fragment of First Order Modal Logic: Two Variable Term Modal Logic, An event-based fragment of first-order logic over intervals, Unnamed Item, Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic, Unnamed Item, Complexity of two-variable dependence logic and IF-logic, Quantitative Logic Reasoning, A Note on C² Interpreted over Finite Data-Words, Two variable first-order logic over ordered domains, Model Checking Games, Comparing the succinctness of monadic query languages over finite trees, Fixed-Point Definability and Polynomial Time on Chordal Graphs and Line Graphs, Group announcement logic, Unnamed Item, Unnamed Item, On the Restraining Power of Guards, First-order definable counting-only queries, Undecidability of First-Order Intuitionistic and Modal Logics with Two variables, Complexity of the two-variable fragment with counting quantifiers, Regular Graphs and the Spectra of Two-Variable Logic with Counting

Cites Work

• A finite model theorem for the propositional \(\mu\)-calculus
• A calculus of communicating systems
• Complexity results for classes of quantificational formulas
• Bounded variable logics: Two, three, and more
• Remarks on Berger's paper on the domino problem
• Undecidable theories
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• On languages with two variables
• On the Decision Problem for Two-Variable First-Order Logic
• On the Restraining Power of Guards
• Undecidability results on two-variable logics
• The undecidability of the domino problem
• On model checking for the \(\mu\)-calculus and its fragments
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item