Q1. ¿Cuáles son las técnicas "estándar" (si las hay) utilizadas para demostrar que un conjunto de vectores en $\mathbb{N}^k$ definido mediante un conjunto de restricciones entre los componentes es (o no es) un conjunto semilineal (es decir, una unión finita de conjuntos lineales)?
Por ejemplo, dado:
$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) ]\} $
cómo puedo (des)demostrar que $A$ es semilineal?
Q2. ¿Puede automatizarse este proceso suponiendo que las condiciones se den mediante un conjunto de expresiones lógicas con constantes y operadores numéricos $\land, \lor, +, -, =, \neq, \leq$ ? Y si se puede automatizar, ¿cuál es su complejidad (computacional)?
0 votos
Estos son los conjuntos definibles en la aritmética de Presburgo es.m.wikipedia.org/wiki/Presburger_arithmetic . También son las imágenes conmutativas de los lenguajes libres de contexto.
0 votos
@BenjaminSteinberg: gracias, me faltaba el teorema (Ginsburg & Spanier) Un predicado es semilineal si y sólo si corresponde a una fórmula de la aritmética de Presburger. Mi ejemplo se vuelve trivial: $x \equiv_k y$ si $\exists z (x + z+z+...^{\text{k times}}...+z = y)$ y $A$ es semilineal. Si lo publicas como respuesta lo aceptaré.
0 votos
Hice lo que me pediste.