Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words
From MaRDI portal
Publication:3395099
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Model theory of finite structures (03C13) Automata and formal grammars in connection with logical questions (03D05) Temporal logic (03B44) Basic properties of first-order languages and structures (03C07) Descriptive complexity and finite models (68Q19)
Abstract: It is well-known that every first-order property on words is expressible using at most three variables. The subclass of properties expressible with only two variables is also quite interesting and well-studied. We prove precise structure theorems that characterize the exact expressive power of first-order logic with two variables on words. Our results apply to both the case with and without a successor relation. For both languages, our structure theorems show exactly what is expressible using a given quantifier depth, n, and using m blocks of alternating quantifiers, for any m leq n. Using these characterizations, we prove, among other results, that there is a strict hierarchy of alternating quantifiers for both languages. The question whether there was such a hierarchy had been completely open. As another consequence of our structural results, we show that satisfiability for first-order logic with two variables without successor, which is NEXP-complete in general, becomes NP-complete once we only consider alphabets of a bounded size.
Recommendations
- Structure Theorem and Strict Alternation Hierarchy for FO2 on Words
- Algebraic characterization of the alternation hierarchy in \(\mathrm{FO}^2[<]\) on finite words
- Quantifier alternation in two-variable first-order logic with successor is decidable
- On FO 2 Quantifier Alternation over Words
- The \(\mathrm{FO}^2\) alternation hierarchy is decidable
Cited in
(24)- Deciding \(\mathrm{FO}^2\) alternation for automata over finite and infinite words
- Testing Simon's congruence
- scientific article; zbMATH DE number 2102756 (Why is no real title available?)
- Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
- Finite-degree predicates and two-variable first-order logic
- On the lattice of sub-pseudovarieties of DA.
- The word problem for omega-terms over the Trotter-Weil hierarchy
- Forbidden Patterns for FO2 Alternation Over Finite and Infinite Words
- Expressive power of existential first-order sentences of Büchi's sequential calculus
- The half-levels of the \(\mathrm {FO}_2\) alternation hierarchy
- The Word Problem for Omega-Terms over the Trotter-Weil Hierarchy
- On the strictness of the quantifier structure hierarchy in first-order logic
- On Simon's congruence closure of a string
- Alternation hierarchies of first order logic with regular predicates
- Matching patterns with variables under Simon's congruence
- Simon's congruence pattern matching
- Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
- Alternating complexity of counting first-order logic for the subword order
- On FO 2 Quantifier Alternation over Words
- Conelikes and ranker comparisons
- Structure Theorem and Strict Alternation Hierarchy for FO2 on Words
- Algebraic characterization of the alternation hierarchy in \(\mathrm{FO}^2[<]\) on finite words
- Two variable vs. linear temporal logic in model checking and games
- scientific article; zbMATH DE number 7269244 (Why is no real title available?)
This page was built for publication: Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3395099)
