From: José María Blasco Comellas Teoría de Conjuntos Efectiva ----------------------------------------- Descripción del problema. Sea L el lenguaje de la Teoría de Conjuntos con igualdad, axiomatizada con una versión débil de Kripke-Platek T. Dado un fragmento F de las Matemáticas (entendidas como representables en la Teoría de Conjuntos), por ejemplo la generación del Universo Constructible, obtener efectivamente y dar el listado completo del subconjunto finito de T necesario para la demostración de los teoremas de F. De este modo obtenemos para F una axiomatización finita y explícita, que puede ser a su vez sometida (sintácticamente) a estudio, para determinar nuevas propiedades de F, construir contramodelos, etc. Métodos de computación utilizados. Las fórmulas de la teoría de conjuntos pura se representan naturalmente mediante una abstracción orientada a objetos. Nuestro prototipo experimental implementa una serie de metafunciones que reflejan las transformaciones sintácticas que el matemático efectúa cotidianamente cuando realiza una demostración. Muchas de estas transformaciones están encaminadas a "mejorar" la forma lógica de una fórmula de L, en el sentido de convertirla, si ello es posible en una fórmula Sigma_1 (o Pi_1). Nuestro prototipo incluye un optimizador especializado en este objetivo. Principales dificultades: Las dificultades encontradas son de dos clases: A) dificultades de orden matemático: es evidente que para que los resultados que obtenemos tengan algún interés, los fórmulas en juego deberán ser, en algún sentido, minimales. Ahora bien: la clase de las fórmulas Delta_0 no admite un orden lineal. Sin embargo, algunas optimizaciones son posibles. B) dificultades de orden informático: 1) dado que nos vemos obligados a traducir las nociones definidas a sus componentes (y estos componentes a sus propios compònentes, en caso de que a su vez incorporen nociones definidas, etc.), obtenemos fórmulas de gran tamaño y manejo difícil. 2) Debemos fijar una demostración determinada entre las varias posibles para cada uno de los teoremas involucrados, ya que los axiomas de T necesarios para la prueba serán distintos cuando la demostración cambie. En su conjunto, 1) y 2) hacen que debamos manejar conjuntos relativamente grandes de fórmulas muy grandes, para lo que se precisa absolutamente de la asistencia de un programa. En general, disponemos de algoritmos lineales para casi todas las operaciones que precisamos. La optimización automática de fórmulas es otro problema, que estamos estudiando.