CONICET | Buscador de Institutos y Recursos Humanos

En 1948, Tarski planteó el problema de decisión para la teoría de primer orden sobre los reales extendida con exponenciación. El problema fue resuelto parcialmente por Macintire y Wilkie en 1996 bajo la hipótesis de que la conjetura de Schanuel es válida y, más recientemente, fue considerado desde el punto de vista algorítmico para fragmentos de la teoría, desarrollándose métodos numéricos para su resolución aunque sin un estudio de la complejidad.En este marco, analizamos el problema de decisión para fórmulas de primer orden que involucran funciones Pfaffianas en una variable de orden 1. Presentamos un algoritmo simbólico nuevo con estimaciones de complejidad para la resolución de este problema que generaliza los procedimientos conocidos para fórmulas que sólo involucran polinomios sobre R. Para funciones Pfaffianas de orden 1 arbitrarias, como es habitual en la literatura, utilizamos un oráculo para determinar el signo que una función toma en un número algebraico. Para el caso particular de E-polinomios, aplicando herramientas desarrolladas previamente, obtenemos un algoritmo para resolver el problema sin necesidad de un oráculo y con estimaciones explícitas de complejidad.

enviar mensaje