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 complexityfinite modelfragment of first-order logicNEXPTIME-completesatisfiability problem for FO\(^ 2\)size of a model

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Model theory of finite structures (03C13) 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

• 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
• 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?)
• 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 complexity of propositional linear temporal logics
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• 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

(only showing first 100 items - show all)

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

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)