Um procedimento eficiente de eliminação de quantificadores para aritmética de Presburger

Todos os procedimentos conhecidos de eliminação de quantificadores para a aritmética de Presburger requerem tempo exponencial duplo para eliminar um único bloco de variáveis quantificadas existencialmente. Afirma-se até na literatura que esse limite superior é apertado. Observamos que essa afirmação está incorreta e desenvolvemos, como resultado principal deste artigo, um procedimento de eliminação de quantificadores que elimina um bloco de variáveis quantificadas existencialmente em tempo exponencial simples. Como corolários, podemos estabelecer a complexidade precisa de numerosos problemas. Exemplos incluem decidir (i) a decomponibilidade monádica para fórmulas existenciais, (ii) se uma fórmula existencial define uma ordenação bem-quasi ou, mais geralmente, (iii) certas fórmulas da aritmética de Presburger com quantificadores de Ramsey. Além disso, apesar do crescimento exponencial, nosso procedimento demonstra que sob suposições brandas, até limites superiores NP para problemas de decisão sobre fórmulas sem quantificadores podem ser transferidos para fórmulas existenciais. A base técnica dos nossos resultados é uma espécie de propriedade de pequeno modelo para programação inteira paramétrica que generaliza os resultados seminais de von zur Gathen e Sieveking sobre pequenos pontos inteiros em poliedros convexos.