Estoy buscando un software que puede encontrar un mínimo global de una función polinómica en R^n más de una poliédrica de dominio (dado por algunos desigualdades lineales decir). El número de variables n no es más que una docena. Sé que se puede hacer en teoría (por Tarski de la eliminación de cuantificadores en verdaderos campos cerrados), y sé que el tiempo, la complejidad es horrible. Sin embargo, si hay una decente aplicación que puede manejar una docena de variables con una interfaz limpia, sería genial. He intentado builtin implementaciones en Mathematica y Maple, y que no parecen terminar en 4-5 variable de instancias.
Si el software puede producir algún tipo de conciso "certificado" de su respuesta, sería aún mejor, pero no estoy seguro de cómo dicho certificado debe parecer ni siquiera en teoría.
Edit: la Convergencia hacia el óptimo es agradable, pero lo que realmente estoy buscando es la capacidad para responder a las preguntas de la forma "Es mínima igual a 5?", donde 5 es lo que yo creo que a priori a ser la respuesta para la optimización de ser (en particular, es un número racional). Eso también explica por qué quiero un certificado/constancia de la desigualdad, o un contraejemplo si es falso.
