Two-variable logic with a between relation

DOI10.1145/2933575.2935308MaRDI QIDQ4635866zbMATH OpenOpenAlexWikidataFDO

Authors A. Krebs, Kamal Lodaya, Paritosh K. Pandya, Howard Straubing

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.05625

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Temporal logic (03B44) Automata and formal grammars in connection with logical questions (03D05) Analysis of algorithms and problem complexity (68Q25) Algebraic theory of languages and automata (68Q70)

Abstract: We study an extension of FO^2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, `the letter a appears between positions x and y'. This is, in a sense, the simplest property that is not expressible using only two variables. We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of satisfiability for each of these formulations. We also give an effective necessary condition, in terms of the syntactic monoid of a regular language, for a property to be expressible in this logic. We show that this condition is also sufficient for words over a two-letter alphabet. This algebraic analysis allows us us to prove, among other things, that our new logic has strictly less expressive power than full first-order logic FO[<].

Recommendations

• Two-variable first order logic with modular predicates over words
• First-order logic with two variables and unary temporal logic
• Two-variable logic with two order relations
• Complexity of two-variable logic on finite trees
• Complexity of two-variable logic on finite trees

Cited in

(9)

• Two-variable first order logic with modular predicates over words
• scientific article; zbMATH DE number 7533353 (Why is no real title available?)
• One-Dimensional Logic over Trees
• Two-variable logics with some betweenness relations: expressiveness, satisfiability and membership
• Reversible regular languages: logical and algebraic characterisations
• Unary and two-variable interval logics
• A generic characterization of generalized unary temporal logic and two-variable first-order logic
• In orbit with MeSCaL: higher in concatenation and navigational hierarchies of regular languages
• A first taste of MeSCaL, a tool for solving membership problems for regular languages

This page was built for publication: Two-variable logic with a between relation

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