# Techniques to (dis)prove that a set is semilinear

Q1. What are the "standard" techniques (if any) used to prove that a set of vectors in $$\mathbb{N}^k$$ defined using a set of constraints among the components is (or is not) a semilinear set (i.e. a finite union of linear sets) ?

For example, given:

$$A = \{ \langle x_1, x_2, x_3, x_4, x_5, x_6 \rangle \mid \sum_i x_i \equiv 0 \bmod 6 \land [x_1 + x_2 + x_3 \neq x_4+x_5+x_6] \land [(x_1 + x_2 \neq x_3 + x_4) \lor (x_3 + x_4 \neq x_5 + x_6) ]\}$$

how can I (dis)prove that $$A$$ is semilinear?

Q2. Can this process be automated assuming that the conditions are given using a set of logic expressions with numeric constants and operators $$\land, \lor, +, -, =, \neq, \leq$$? And if it can be automated, what is its (computational) complexity?

• These are the definable sets in Presburger arithmetic en.m.wikipedia.org/wiki/Presburger_arithmetic. They are also the commutative images of context free languages. – Benjamin Steinberg Jan 25 '19 at 20:41
• @BenjaminSteinberg: thanks, I was missing the theorem (Ginsburg & Spanier) A predicate is semi-linear if and only if it corresponds to a formula of Presburger’s arithmetic. My example becomes trivial: $x \equiv_k y$ iff $\exists z (x + z+z+...^{\text{k times}}...+z = y)$; and $A$ is semilinear. If you post it as an answer I'll accept it. – Marzio De Biasi Jan 25 '19 at 21:38
• I did what you asked. – Benjamin Steinberg Jan 25 '19 at 21:44