Quería encontrar el conjunto semialgebraico en el $(a_0,a_1,a_2,a_3)$ espacio que garantiza que existe al menos una raíz real de la ecuación polinómica general de grado 4. Para ello, instalando QEPCAD en Ubuntu 14, intenté eliminar el único cuantificador existencial en
$\exists x[x^4 + a_3 x^3 + a_2 x^2 + a_1 x + a_0 = 0]$
Dando entrada sucesiva como
hizo QEPCAD pensar durante varios minutos, y luego fallar, debido a la falta de memoria supongo (en realidad un problema similar se encuentra entre los ejemplos en el sitio QEPCAD, http://www.usna.edu/CS/qepcadweb/B/examples/Quartic/Quartic.html Pero incluso aumentando, para ese problema, el +N del valor por defecto a +N80000000, no ayudó).
Ahora la complejidad de los algoritmos conocidos de eliminación de cuantificadores, según http://mathworld.wolfram.com/QuantifierElimination.html por ejemplo, es malo (doblemente exponencial asintóticamente, al menos en el número de alternancias de cuantificadores), pero pensé que para un problema de aspecto tan simple, la respuesta se obtendría sin embargo con relativa rapidez.
Entonces, ¿la situación con estos algoritmos es realmente tan mala desde un punto de vista práctico? Buscando referencias sobre cuestiones de aplicación práctica, he encontrado que algunos hablan de "aplicaciones en la industria" (por ejemplo http://www.issac-symposium.org/2014/tutorials/ISSAC2014_tutorial_handout_Anai.pdf ), pero los ejemplos traídos en el texto (ojeando superficialmente el texto) no parecían mucho más complicados que el anterior.
EDITAR: tal vez hubo algún problema de entorno, o un problema con la sintaxis precisa que utilicé, aunque no recibí ningún mensaje de error con respecto a la sintaxis, u otro error que cometí (voy a tratar de entender lo que pasó, y luego editar la pregunta de nuevo). Ahora mismo he conseguido, después de muy poco tiempo, eliminar los cuantificadores de
$\exists x[x^4 + a x^3 + b x^2 + c x + d = 0]$
EDITAR:
bueno, las cosas son más complicadas.. En primer lugar, el programa QEPCAD es interactivo, y el usuario aparentemente puede especificar diferentes opciones en la línea de comandos en varias etapas de la búsqueda de una solución. No pude encontrar la documentación de estas opciones en el sitio de QEPCAD (tal vez no busqué lo suficientemente bien). En segundo lugar, la capacidad de QEPCAD para eliminar cuantificadores en la fórmula que especifiqué depende de los nombres de las variables (lo que significa probablemente que depende del orden de las variables, http://staff.bath.ac.uk/masjhd/ISSACs/ISSAC07-final.pdf ), por lo que $\exists x[x^4 + a x^3 + b x^2 + c x + d = 0]$ se resolvió en 1 segundo más o menos, pero $\exists x[x^4 + d x^3 + c x^2 + b x + a = 0]$ no lo era (todavía estoy esperando a que salga la solución, es decir, después de haber insertado "go" en la línea de comandos cada vez que se esperaba una entrada interactiva).
Parece que se ha invertido un esfuerzo considerable en QEPCAD, pero tal como está, es difícil de utilizar por un no experto (y no he encontrado ninguna documentación detallada). Me pregunto si existe algún software comercial que sea sustancialmente mejor (y por cierto, ¿cuál es ese software comercial? ¿MAPLE?).
