Q1. ¿Cuáles son las técnicas "estándar" (si las hay) utilizadas para demostrar que un conjunto de vectores en Nk 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.