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

DOI10.2307/421196zbMath0873.03009OpenAlexW2124580444MaRDI QIDQ4338040

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

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

Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Model theory of finite structures (03C13) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Two-Variable Logic with Counting and Trees ⋮ Complexity of Two-Variable Logic on Finite Trees ⋮ Finite Variable Logics in Descriptive Complexity Theory ⋮ The guarded fragment with transitive guards ⋮ Adding one or more equivalence relations to the interval temporal logic \(\mathsf{AB}\overline{\mathsf{B}}\) ⋮ The Range of Modal Logic ⋮ Bounded model checking of infinite state systems ⋮ The decision problem of modal product logics with a diagonal, and faulty counter machines ⋮ Undecidability of QLTL and QCTL with two variables and one monadic predicate letter ⋮ The two‐variable fragment with counting and equivalence ⋮ Metric propositional neighborhood logic with an equivalence relation ⋮ Small substructures and decidability issues for first-order logic with two variables ⋮ On the complexity of the two-variable guarded fragment with transitive guards ⋮ A description logic based situation calculus ⋮ Separation logics and modalities: a survey ⋮ Integrity constraints for XML ⋮ Бинарный предикат, транзитивное замыкание, две-три переменные: сыграем в домино? ⋮ A Decidable Fragment of First Order Modal Logic: Two Variable Term Modal Logic ⋮ Lifted inference with tree axioms ⋮ Two-Variable Separation Logic and Its Inner Circle ⋮ Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting ⋮ Finite satisfiability for two‐variable, first‐order logic with one transitive relation is decidable ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Automatic conjecturing of P-recursions using lifted inference ⋮ Uniform guarded fragments ⋮ An event-based fragment of first-order logic over intervals ⋮ Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions ⋮ Computational complexity of theories of a binary predicate with a small number of variables ⋮ On logics with two variables ⋮ Lattice logic as a fragment of (2-sorted) residuated modal logic ⋮ Complexity of two-variable dependence logic and IF-logic ⋮ On the complexity of team logic and its two-variable fragment ⋮ Quantitative Logic Reasoning ⋮ The fluted fragment with transitive relations ⋮ Two variable first-order logic over ordered domains ⋮ Using tableau to decide description logics with full role negation and identity ⋮ Goals and benchmarks for automated map reasoning ⋮ Logics for Two Fragments beyond the Syllogistic Boundary ⋮ All normal extensions of S5-squared are finitely axiomatizable ⋮ Undecidability results on two-variable logics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ THE FLUTED FRAGMENT REVISITED ⋮ Unnamed Item ⋮ First-order logic with two variables and unary temporal logic ⋮ Decidability of cylindric set algebras of dimension two and first-order logic with two variables ⋮ On the Restraining Power of Guards ⋮ Statistical \(\mathcal{EL}\) is \textsc{ExpTime}-complete ⋮ A simple combinatorial proof for the small model property of two-variable logic ⋮ The Complexity of Decomposing Modal and First-Order Theories ⋮ Modal translation of substructural logics ⋮ Description Logics ⋮ The Fluted Fragment with Transitivity ⋮ Combinations of Theories for Decidable Fragments of First-Order Logic ⋮ Products of Modal Logics with Diagonal Constant Lacking the Finite Model Property ⋮ Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter ⋮ Deciding regular grammar logics with converse through first-order logic ⋮ LOGICS FOR THE RELATIONAL SYLLOGISTIC ⋮ Logical separability of labeled data examples under ontologies ⋮ REDUCTION TECHNIQUES FOR PROVING DECIDABILITY IN LOGICS AND THEIR MEET–COMBINATION ⋮ Path constraints in semistructured databases ⋮ SGGS decision procedures ⋮ On the Blok-Esakia Theorem ⋮ Modal Satisfiability via SMT Solving ⋮ Regular Graphs and the Spectra of Two-Variable Logic with Counting ⋮ Deciding the guarded fragments by resolution

Cites Work