Demostración automatizada de teoremas

La demostración automatizada de teoremas (también conocida como ATP o deducción automatizada ) es un subcampo del razonamiento automatizado y la lógica matemática que se ocupa de demostrar teoremas matemáticos mediante programas informáticos . El razonamiento automatizado sobre la demostración matemática fue un factor motivador importante para el desarrollo de la informática .

Si bien las raíces de la lógica formalizada se remontan a Aristóteles , a finales del siglo XIX y principios del XX se desarrolló la lógica moderna y las matemáticas formalizadas. El Begriffsschrift (1879) de Frege introdujo tanto un cálculo proposicional completo como lo que es esencialmente la lógica de predicados moderna . ^{[ 1 ]} Su Foundations of Arithmetic , publicado en 1884, ^{[ 2 ]} expresó (partes de) las matemáticas en lógica formal. Este enfoque fue continuado por Russell y Whitehead en su influyente Principia Mathematica , publicado por primera vez entre 1910 y 1913, ^{[ 3 ]} y con una segunda edición revisada en 1927. ^{[ 4 ]} Russell y Whitehead pensaron que podían derivar toda la verdad matemática utilizando axiomas y reglas de inferencia de la lógica formal, abriendo en principio el proceso a la automatización. ^{[ 5 ]} En 1920, Thoralf Skolem simplificó un resultado previo de Leopold Löwenheim , dando lugar al teorema de Löwenheim-Skolem y, en 1930, a la noción de un universo de Herbrand y una interpretación de Herbrand que permitía reducir la (in)satisfacibilidad de fórmulas de primer orden (y por lo tanto la validez de un teorema) a (potencialmente infinitos) problemas de satisfacibilidad proposicional. ^{[ 6 ]}

En 1929, Mojżesz Presburger demostró que la teoría de primer orden de los números naturales con suma e igualdad (ahora llamada aritmética de Presburger en su honor) es decidible y proporcionó un algoritmo que podía determinar si una oración dada en el lenguaje era verdadera o falsa. ^{[ 7 ] [ 8 ]}

Sin embargo, poco después de este resultado positivo, Kurt Gödel publicó Sobre proposiciones formalmente indecidibles de Principia Mathematica y sistemas relacionados (1931), demostrando que en cualquier sistema axiomático suficientemente fuerte existen enunciados verdaderos que no pueden probarse en dicho sistema. ^{[ 9 ]} Este tema fue desarrollado posteriormente en la década de 1930 por Alonzo Church y Alan Turing , quienes, por un lado, dieron dos definiciones independientes pero equivalentes de computabilidad y, por otro, proporcionaron ejemplos concretos de cuestiones indecidibles . ^{[ 10 ]}

En 1954, Martin Davis programó el algoritmo de Presburger para una computadora de tubos de vacío JOHNNIAC en el Instituto de Estudios Avanzados de Princeton, Nueva Jersey. Según Davis, "Su gran triunfo fue demostrar que la suma de dos números pares es par". ^{[ 8 ] [ 11 ]} Más ambicioso fue el Logic Theorist en 1956, un sistema de deducción para la lógica proposicional de los Principia Mathematica , desarrollado por Allen Newell , Herbert A. Simon y JC Shaw . También ejecutándose en un JOHNNIAC, el Logic Theorist construyó demostraciones a partir de un pequeño conjunto de axiomas proposicionales y tres reglas de deducción: modus ponens , sustitución de variables (proposicionales) y reemplazo de fórmulas por su definición. El sistema utilizó guía heurística y logró demostrar 38 de los primeros 52 teoremas de los Principia . ^{[ 8 ]}

El enfoque "heurístico" del teórico de la lógica intentó emular a los matemáticos humanos y no pudo garantizar que se pudiera encontrar una demostración para cada teorema válido, ni siquiera en principio. En contraste, otros algoritmos más sistemáticos lograron, al menos teóricamente, la completitud para la lógica de primer orden. Los enfoques iniciales se basaron en los resultados de Herbrand y Skolem para convertir una fórmula de primer orden en conjuntos sucesivamente mayores de fórmulas proposicionales instanciando variables con términos del universo de Herbrand . Luego, se podía verificar la insatisfacibilidad de las fórmulas proposicionales utilizando varios métodos. El programa de Gilmore utilizó la conversión a la forma normal disyuntiva , una forma en la que la satisfacibilidad de una fórmula es obvia. ^{[ 8 ] [ 12 ]}

Dependiendo de la lógica subyacente, el problema de decidir la validez de una fórmula varía de trivial a imposible. Para el caso común de la lógica proposicional , el problema es decidible pero co-NP-completo , y por lo tanto, se cree que solo existen algoritmos de tiempo exponencial para tareas de prueba generales. ^{[ 13 ]} Para un cálculo de predicados de primer orden , el teorema de completitud de Gödel establece que los teoremas (enunciados demostrables) son exactamente las fórmulas bien formadas semánticamente válidas , por lo que las fórmulas válidas son computacionalmente enumerables : dados recursos ilimitados, cualquier fórmula válida puede eventualmente ser demostrada. Sin embargo, las fórmulas inválidas (aquellas que no están implicadas por una teoría dada) no siempre pueden ser reconocidas. ^{[ 14 ]}

Lo anterior se aplica a teorías de primer orden, como la aritmética de Peano . Sin embargo, para un modelo específico que puede describirse mediante una teoría de primer orden, algunas afirmaciones pueden ser verdaderas pero indecidibles en la teoría utilizada para describir el modelo. Por ejemplo, según el teorema de incompletitud de Gödel , sabemos que cualquier teoría consistente cuyos axiomas sean verdaderos para los números naturales no puede probar que todas las afirmaciones de primer orden sean verdaderas para los números naturales, incluso si se permite que la lista de axiomas sea infinitamente enumerable. ^{[ 15 ]} De ello se deduce que un demostrador automático de teoremas no terminará mientras busca una prueba precisamente cuando la afirmación que se está investigando sea indecidible en la teoría que se está utilizando, incluso si es verdadera en el modelo de interés. A pesar de este límite teórico, en la práctica, los demostradores de teoremas pueden resolver muchos problemas difíciles, incluso en modelos que no están completamente descritos por ninguna teoría de primer orden (como los enteros ).

Un problema más sencillo, aunque relacionado, es la verificación de pruebas , donde se certifica la validez de una prueba existente para un teorema. Para ello, generalmente se requiere que cada paso de la prueba pueda verificarse mediante una función o programa recursivo primitivo , por lo que el problema siempre es decidible.

Dado que las demostraciones generadas por los demostradores automáticos de teoremas suelen ser muy extensas, el problema de la compresión de pruebas es crucial, y se han desarrollado diversas técnicas destinadas a reducir el tamaño de la salida del demostrador y, en consecuencia, hacerla más fácil de entender y verificar.

Los asistentes de demostración requieren que un usuario humano proporcione pistas al sistema. Dependiendo del grado de automatización, el demostrador puede reducirse esencialmente a un verificador de pruebas, donde el usuario proporciona la prueba de manera formal, o bien, tareas de demostración significativas pueden realizarse automáticamente. Los demostradores interactivos se utilizan para diversas tareas, pero incluso los sistemas totalmente automáticos han demostrado varios teoremas interesantes y difíciles, incluyendo al menos uno que ha eludido a los matemáticos humanos durante mucho tiempo, a saber, la conjetura de Robbins . ^{[ 16 ] [ 17 ]} Sin embargo, estos éxitos son esporádicos, y el trabajo en problemas difíciles generalmente requiere un usuario competente.

A veces se establece otra distinción entre la demostración de teoremas y otras técnicas, donde un proceso se considera demostración de teoremas si consiste en una demostración tradicional, partiendo de axiomas y generando nuevos pasos de inferencia mediante reglas de inferencia. Otras técnicas incluirían la verificación de modelos , que, en el caso más simple, implica la enumeración por fuerza bruta de muchos estados posibles (aunque la implementación real de los verificadores de modelos requiere mucha astucia y no se reduce simplemente a la fuerza bruta).

Existen sistemas híbridos de demostración de teoremas que utilizan la verificación de modelos como regla de inferencia. También hay programas diseñados para demostrar un teorema específico, con una prueba (generalmente informal) que establece que si el programa finaliza con un resultado determinado, entonces el teorema es verdadero. Un buen ejemplo de esto fue la demostración asistida por máquina del teorema de los cuatro colores , que resultó muy controvertida, ya que la primera demostración matemática que se presentó era prácticamente imposible de verificar por humanos debido al enorme tamaño del cálculo del programa (estas demostraciones se denominan demostraciones no verificables ). Otro ejemplo de demostración asistida por programa es la que muestra que el juego de Conecta Cuatro siempre puede ser ganado por el primer jugador.

El uso comercial de la demostración automatizada de teoremas se concentra principalmente en el diseño y la verificación de circuitos integrados . Desde el error FDIV del Pentium , las complejas unidades de punto flotante de los microprocesadores modernos se han diseñado con un escrutinio adicional. AMD , Intel y otros utilizan la demostración automatizada de teoremas para verificar que la división y otras operaciones se implementen correctamente en sus procesadores. ^{[ 18 ]}

Otros usos de los demostradores de teoremas incluyen la síntesis de programas , la construcción de programas que satisfacen una especificación formal . ^{[ 19 ]} Los demostradores de teoremas automatizados se han integrado con asistentes de prueba , incluido Isabelle/HOL . ^{[ 20 ]}

Las aplicaciones de los demostradores de teoremas también se encuentran en el procesamiento del lenguaje natural y la semántica formal , donde se utilizan para analizar representaciones del discurso . ^{[ 21 ] [ 22 ]}

A finales de la década de 1960, las agencias que financiaban la investigación en deducción automatizada comenzaron a enfatizar la necesidad de aplicaciones prácticas. Una de las primeras áreas fructíferas fue la de la verificación de programas, donde se aplicaron demostradores de teoremas de primer orden al problema de verificar la corrección de programas informáticos en lenguajes como Pascal , Ada , etc. Entre los primeros sistemas de verificación de programas, destacó el Stanford Pascal Verifier, desarrollado por David Luckham en la Universidad de Stanford . ^{[ 23 ] [ 24 ] [ 25 ]} Este se basó en el Stanford Resolution Prover, también desarrollado en Stanford, utilizando el principio de resolución de John Alan Robinson . Este fue el primer sistema de deducción automatizada que demostró la capacidad de resolver problemas matemáticos anunciados en los Notices of the American Mathematical Society antes de que se publicaran formalmente las soluciones.

La demostración de teoremas de primer orden es uno de los subcampos más maduros de la demostración automatizada de teoremas. La lógica es lo suficientemente expresiva como para permitir la especificación de problemas arbitrarios, a menudo de una manera razonablemente natural e intuitiva. Por otro lado, sigue siendo semidecidible, y se han desarrollado varios cálculos sólidos y completos que permiten sistemas totalmente automatizados. ^{[ 26 ]} Las lógicas más expresivas, como las lógicas de orden superior , permiten la expresión conveniente de una gama más amplia de problemas que la lógica de primer orden, pero la demostración de teoremas para estas lógicas está menos desarrollada. ^{[ 27 ] [ 28 ]}

La calidad de los sistemas implementados se ha beneficiado de la existencia de una gran biblioteca de ejemplos de referencia estándar —la Biblioteca de problemas Thousands of Problems for Theorem Provers (TPTP) ^{[ 31 ]} — así como de la CADE ATP System Competition (CASC), una competición anual de sistemas de primer orden para muchas clases importantes de problemas de primer orden.

A continuación se enumeran algunos sistemas importantes (todos ellos han ganado al menos una división de la competición CASC).

• E es un demostrador de alto rendimiento para lógica de primer orden completa, pero construido sobre un cálculo puramente ecuacional , desarrollado originalmente en el grupo de razonamiento automatizado de la Universidad Técnica de Múnich bajo la dirección de Wolfgang Bibel , y ahora en la Universidad Estatal Cooperativa de Baden-Württemberg en Stuttgart .
• Otter , desarrollado en el Laboratorio Nacional Argonne , se basa en la resolución de primer orden y la paramodulación . Posteriormente, Otter fue reemplazado por Prover9 , que se combina con Mace4 .
• SETHEO es un sistema de alto rendimiento basado en el cálculo de eliminación de modelos orientado a objetivos , desarrollado originalmente por un equipo dirigido por Wolfgang Bibel . E y SETHEO se han combinado (con otros sistemas) en el demostrador de teoremas compuesto E-SETHEO.
• Vampire fue desarrollado e implementado originalmente en la Universidad de Manchester por Andrei Voronkov y Kryštof Hoder. Actualmente, su desarrollo corre a cargo de un equipo internacional en constante crecimiento. Ha ganado la división FOF (entre otras divisiones) en la competición CADE ATP System desde 2001 de forma regular. ^{[ 32 ]}
• Waldmeister es un sistema especializado para la lógica de primer orden con ecuaciones unitarias, desarrollado por Arnim Buch y Thomas Hillenbrand. Ganó la división UEQ de CASC durante catorce años consecutivos (1997-2010).
• SPASS es un demostrador de teoremas de lógica de primer orden con igualdad. Ha sido desarrollado por el grupo de investigación Automatización de la Lógica del Instituto Max Planck de Ciencias de la Computación .

El Museo de Demostradores de Teoremas ^{[ 33 ]} es una iniciativa para conservar las fuentes de los sistemas de demostración de teoremas para su análisis futuro, dado que constituyen importantes artefactos culturales y científicos. Contiene las fuentes de muchos de los sistemas mencionados anteriormente.

• Resolución de primer orden con unificación
• Eliminación del modelo
• Método de cuadros analíticos
• Superposición y reescritura de términos
• Verificación de modelos
• Inducción matemática ^{[ 34 ]}
• Diagramas de decisión binaria
• DPLL
• Unificación de orden superior
• Eliminación de cuantificadores ^{[ 35 ]}
• Grandes modelos de lenguaje ^{[ 36 ]}

• Una lista de herramientas para la demostración de teoremas