Addition-Invariant FO and Regularity

We consider formulas which, in addition to the symbols in the vocabulary, may use two designated symbols ≺ and + that must be interpreted as a linear order and its associated addition. Such a formula is called addition-invariant if, for each fixed interpretation of the initial vocabulary, its result is independent of the particular interpretation of ≺ and +. This paper studies the expressive power of additioninvariant first-order logic, +-inv-FO, on the class of finite strings. Our first main result gives a characterization of the regular languages definable in +-inv-FO: we show that these are exactly the languages definable in FO with extra predicates, denoted by “lm” for short, for testing the length of the string modulo some fixed number. Our second main result shows that every language definable in +-inv-FO, that is bounded or commutative or deterministic context-free, is regular. As an immediate consequence of these two main results, we obtain that +-inv-FO is equ...

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Nicole Schweikardt, Luc Segoufin
• Keywords: Additioninvariant first-order Logic, Algebraic Automata Theory, Automated Reasoning, LICS 2010, finite Colored Sets