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

DOI10.2307/421196MaRDI QIDQ4338040zbMATH OpenOpenAlexFDO

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

Publication date 30 June 1997

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

Full work available at URL https://semanticscholar.org/paper/24fe6d8f1fdec294278632bedccdc1c5e9fc6234, http://www.math.ucla.edu/~asl/bsl/0301-toc.htm

zbMATH Keywords

computational complexityfragment of first-order logicNEXPTIME-completefinite modelsatisfiability problem for FO\(^ 2\)size of a model

Mathematics Subject Classification ID

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

Recommendations

• On logics with two variables
• Complexity Results for First-Order Two-Variable Logic with Counting
• Small substructures and decidability issues for first-order logic with two variables

Cites work

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

Cited in

(98)

• Combinations of Theories for Decidable Fragments of First-Order Logic
• Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
• A version of predicate logic with two variables that has an incompleteness property
• Data-complexity of the two-variable fragment with counting quantifiers
• scientific article; zbMATH DE number 7566055 (Why is no real title available?)
• Small substructures and decidability issues for first-order logic with two variables
• Lifted algorithms for symmetric weighted first-order model sampling
• Monodic fragments of probabilistic first-order temporal logic with bounded semantics
• Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions
• The two-variable fragment with counting and equivalence
• All normal extensions of S5-squared are finitely axiomatizable
• Two variable logic with ultimately periodic counting
• Two decision problems in Contact Logics
• Separation logics and modalities: a survey
• scientific article; zbMATH DE number 7561661 (Why is no real title available?)
• Decidability of querying first-order theories via countermodels of finite width
• About the expressive power and complexity of order-invariance with two variables
• Description Logics
• On the Restraining Power of Guards
• Deciding regular grammar logics with converse through first-order logic
• scientific article; zbMATH DE number 7561660 (Why is no real title available?)
• Means and limits of decision (invited talk)
• Adding one or more equivalence relations to the interval temporal logic \(\mathsf{AB}\overline{\mathsf{B}}\)
• Lifted inference with tree axioms
• Universal first-order logic is superfluous in the second level of the polynomial-time hierarchy
• Decidability of cylindric set algebras of dimension two and first-order logic with two variables
• The fluted fragment with transitive relations
• Alternating quantifiers in uniform one-dimensional fragments with an excursion into three-variable logic
• Path constraints in semistructured databases
• On the complexity of the two-variable guarded fragment with transitive guards
• The decision problem of modal product logics with a diagonal, and faulty counter machines
• Automatic conjecturing of P-recursions using lifted inference
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• On two-variable guarded fragment logic with expressive local Presburger constraints
• Complexity of two-variable logic on finite trees
• On the complexity of the Bernays-Schönfinkel class with Datalog
• scientific article; zbMATH DE number 1765671 (Why is no real title available?)
• Two variable logic with ultimately periodic counting
• Using tableau to decide description logics with full role negation and identity
• LOGICS FOR THE RELATIONAL SYLLOGISTIC
• Deciding first-order satisfiability when universal and existential variables are separated
• The triguarded fragment with transitivity
• An excursion to the border of decidability: between two- and three-variable logic
• A fine-grained hierarchy of hard problems in the separated fragment
• A simple combinatorial proof for the small model property of two-variable logic
• Statistical \(\mathcal{EL}\) is \textsc{ExpTime}-complete
• Complexity of two-variable dependence logic and IF-logic
• Expressive completeness of separation logic with two variables and no separating conjunction
• Lattice logic as a fragment of (2-sorted) residuated modal logic
• A description logic based situation calculus
• REDUCTION TECHNIQUES FOR PROVING DECIDABILITY IN LOGICS AND THEIR MEET–COMBINATION
• Uniform guarded fragments
• First-order logic with two variables and unary temporal logic
• Metric propositional neighborhood logic with an equivalence relation
• Two-Variable Separation Logic and Its Inner Circle
• The guarded fragment with transitive guards
• Бинарный предикат, транзитивное замыкание, две-три переменные: сыграем в домино?
• On the Blok-Esakia theorem
• Undecidability results on two-variable logics
• On two-variable first-order logic with a partial order
• Computational complexity of theories of a binary predicate with a small number of variables
• Logics for two fragments beyond the syllogistic boundary
• Quantitative logic reasoning
• Modal translation of substructural logics
• A Decidable Fragment of First Order Modal Logic: Two Variable Term Modal Logic
• The fluted fragment revisited
• Deciding the existence of interpolants and definitions in first-order modal logic
• Products of modal logics with diagonal constant lacking the finite model property
• Deciding the guarded fragments by resolution
• Modal Satisfiability via SMT Solving
• Note on a translation from first-order logic into the calculus of relations preserving validity and finite validity
• Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting
• The Complexity of Decomposing Modal and First-Order Theories
• Regular graphs and the spectra of two-variable logic with counting
• On logics with two variables
• Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter
• Complexity of two-variable logic on finite trees
• On the existential fragments of local first-order logics with data
• The Range of Modal Logic
• Two-variable logic with counting and trees
• The ground-negative fragment of first-order logic is -complete
• scientific article; zbMATH DE number 7561674 (Why is no real title available?)
• On homogeneous models of fluted languages
• The Fluted Fragment with Transitivity
• Finite satisfiability for two‐variable, first‐order logic with one transitive relation is decidable
• Two variable first-order logic over ordered domains
• Finite Variable Logics in Descriptive Complexity Theory
• The adjacent fragment and Quine's limits of decision
• Goals and benchmarks for automated map reasoning
• Integrity constraints for XML
• Two variables and two successors
• Logical separability of labeled data examples under ontologies
• SGGS decision procedures
• A uniform one-dimensional fragment with alternation of quantifiers
• An event-based fragment of first-order logic over intervals
• On the complexity of team logic and its two-variable fragment
• scientific article; zbMATH DE number 7533353 (Why is no real title available?)
• Bounded model checking of infinite state systems

This page was built for publication: On the Decision Problem for Two-Variable First-Order Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4338040)