On the Decision Problem for Two-Variable First-Order Logic

DOI10.2307/421196zbMath0873.03009MaRDI QIDQ4338040

Erich Grädel, Moshe Y. Vardi, Phokion G. Kolaitis

Publication date: 30 June 1997

Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/24fe6d8f1fdec294278632bedccdc1c5e9fc6234

zbMATH Keywords

computational complexity; fragment of first-order logic; NEXPTIME-complete; finite model; satisfiability problem for FO\(^ 2\); size of a model

Mathematics Subject Classification ID

03B25: Decidability of theories and sets of sentences

03D15: Complexity of computation (including implicit computational complexity)

03C13: Model theory of finite structures

03B20: Subsystems of classical logic (including intuitionistic logic)

Related Items

The Range of Modal Logic, Decidability of cylindric set algebras of dimension two and first-order logic with two variables, On the Restraining Power of Guards, Goals and benchmarks for automated map reasoning, LOGICS FOR THE RELATIONAL SYLLOGISTIC, A description logic based situation calculus, Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions, On the complexity of the two-variable guarded fragment with transitive guards, Integrity constraints for XML, Path constraints in semistructured databases, All normal extensions of S5-squared are finitely axiomatizable, Deciding the guarded fragments by resolution, The guarded fragment with transitive guards, On logics with two variables, Bounded model checking of infinite state systems, An event-based fragment of first-order logic over intervals, First-order logic with two variables and unary temporal logic, Deciding regular grammar logics with converse through first-order logic, Two variable first-order logic over ordered domains, Small substructures and decidability issues for first-order logic with two variables, Logics for Two Fragments beyond the Syllogistic Boundary, Description Logics, Combinations of Theories for Decidable Fragments of First-Order Logic, Products of Modal Logics with Diagonal Constant Lacking the Finite Model Property, Finite Variable Logics in Descriptive Complexity Theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Satisfiability of formulae with one \(\forall\) is decidable in exponential time
• 0-1 laws and decision problems for fragments of second-order logic
• Definability with bounded number of bound variables
• On the expressive power of Datalog: tools and a case study.
• Automata-theoretic techniques for modal logics of programs
• A near-optimal method for reasoning about action
• Complexity results for classes of quantificational formulas
• Upper and lower bounds for first order expressibility
• A guide to completeness and complexity for modal logics of knowledge and belief
• Infinitary logics and 0-1 laws
• An optimal lower bound on the number of variables for graph identification
• Propositional dynamic logic of regular programs
• Über die Erfüllbarkeit derjenigen Zählausdrücke, welche in der Normalform zwei benachbarte Allzeichen enthalten
• Untersuchungen zum Entscheidungsproblem der mathematischen Logik
• Infinitary logic and inductive definability over finite structures
• Knowledge and common knowledge in a distributed environment
• The unsolvability of the Gödel class with identity
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• The complexity of propositional linear temporal logics
• On languages with two variables
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• Correction to A note on the Entscheidungsproblem