La demostración automática de teoremas (también conocida como ATP o deducción automática ) es un subcampo del razonamiento automático y la lógica matemática que se ocupa de la demostración de teoremas matemáticos mediante programas informáticos . El razonamiento automático sobre la demostración matemática fue un factor motivador importante para el desarrollo de la informática .
Aunque las raíces de la lógica formalizada se remontan a Aristóteles , a finales del siglo XIX y principios del XX se produjo el desarrollo de la lógica moderna y las matemáticas formalizadas. La Begriffsschrift (1879) de Frege introdujo tanto un cálculo proposicional completo como lo que es esencialmente la lógica de predicados moderna . [1] Su Fundamentos de aritmética , 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. En 1920, Thoralf Skolem simplificó un resultado previo de Leopold Löwenheim , lo que condujo 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. [5]
En 1929, Mojżesz Presburger demostró que la teoría de primer orden de los números naturales con adición e igualdad (ahora llamada aritmética de Presburger en su honor) es decidible y dio un algoritmo que podía determinar si una oración dada en el lenguaje era verdadera o falsa. [6] [7]
Sin embargo, poco después de este resultado positivo, Kurt Gödel publicó On Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931), mostrando que en cualquier sistema axiomático suficientemente fuerte hay enunciados verdaderos que no pueden ser probados en el sistema. Este tema fue desarrollado más a fondo 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 dieron ejemplos concretos de cuestiones indecidibles .
Poco después de la Segunda Guerra Mundial , aparecieron las primeras computadoras de propósito general. En 1954, Martin Davis programó el algoritmo de Presburger para una computadora de tubo 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". [7] [8] Más ambicioso fue el Logic Theorist de 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ó pruebas a partir de un pequeño conjunto de axiomas proposicionales y tres reglas de deducción: modus ponens , sustitución de variable (proposicional) y el reemplazo de fórmulas por su definición. El sistema utilizó una guía heurística y logró demostrar 38 de los primeros 52 teoremas de los Principia . [7]
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 prueba 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 más grandes de fórmulas proposicionales mediante la instanciación de variables con términos del universo de Herbrand . Las fórmulas proposicionales luego podían verificarse para determinar su insatisfacción 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. [7] [9]
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. 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 computablemente 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 reconocerse.
Lo anterior se aplica a las teorías de primer orden, como la aritmética de Peano . Sin embargo, para un modelo específico que puede ser descrito por una teoría de primer orden, algunas afirmaciones pueden ser verdaderas pero indecidibles en la teoría utilizada para describir el modelo. Por ejemplo, por 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. De ello se deduce que un demostrador de teoremas automatizado no podrá terminar mientras busca una prueba precisamente cuando la afirmación que se investiga sea indecidible en la teoría que se utiliza, 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 números enteros ).
Un problema más simple, pero relacionado, es la verificación de pruebas , en la que se certifica la validez de una prueba existente para un teorema. Para ello, generalmente se requiere que cada paso de prueba individual pueda verificarse mediante una función o programa recursivo primitivo y, por lo tanto, el problema siempre es decidible.
Dado que las pruebas generadas por los demostradores de teoremas automatizados suelen ser muy grandes, el problema de la compresión de pruebas es crucial, y se han desarrollado varias técnicas destinadas a hacer que la salida del demostrador sea más pequeña y, en consecuencia, más fácilmente comprensible y comprobable.
Los asistentes de prueba requieren que un usuario humano dé pistas al sistema. Dependiendo del grado de automatización, el probador puede reducirse esencialmente a un verificador de pruebas, en el que el usuario proporciona la prueba de manera formal, o se pueden realizar tareas de prueba importantes de forma automática. Los probadores interactivos se utilizan para una variedad de tareas, pero incluso los sistemas completamente automáticos han demostrado una serie de teoremas interesantes y difíciles, incluido al menos uno que ha eludido a los matemáticos humanos durante mucho tiempo, a saber, la conjetura de Robbins . [10] [11] Sin embargo, estos éxitos son esporádicos y el trabajo en problemas difíciles generalmente requiere un usuario competente.
A veces se hace otra distinción entre la demostración de teoremas y otras técnicas, donde un proceso se considera una demostración de teoremas si consiste en una prueba tradicional, que comienza con axiomas y produce nuevos pasos de inferencia utilizando reglas de inferencia. Otras técnicas incluirían la comprobació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 inteligencia y no se reduce simplemente a la fuerza bruta).
Existen sistemas híbridos de demostración de teoremas que utilizan la comprobación de modelos como regla de inferencia. También hay programas que se escribieron para demostrar un teorema en particular, con una prueba (generalmente informal) de que si el programa termina con un resultado determinado, entonces el teorema es verdadero. Un buen ejemplo de esto fue la prueba asistida por máquina del teorema de los cuatro colores , que fue muy controvertida por ser la primera prueba matemática que era esencialmente imposible de verificar por humanos debido al enorme tamaño del cálculo del programa (tales pruebas se denominan pruebas no verificables ). Otro ejemplo de una prueba asistida por programa es la que muestra que el juego de Conecta 4 siempre lo puede ganar el primer jugador.
El uso comercial de la demostración automatizada de teoremas se concentra principalmente en el diseño y verificación de circuitos integrados . Desde el error FDIV de Pentium , las complicadas unidades de punto flotante de los microprocesadores modernos han sido diseñadas 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 implementan correctamente en sus procesadores. [12]
Otros usos de los demostradores de teoremas incluyen la síntesis de programas y la construcción de programas que satisfacen una especificación formal . [13] Los demostradores de teoremas automatizados se han integrado con asistentes de prueba , incluido Isabelle/HOL . [14]
También se encuentran aplicaciones de los demostradores de teoremas en el procesamiento del lenguaje natural y la semántica formal , donde se utilizan para analizar representaciones del discurso . [15] [16]
A finales de los años 1960, las agencias que financiaban la investigación en deducción automática comenzaron a enfatizar la necesidad de aplicaciones prácticas. [ cita requerida ] Una de las primeras áreas fructíferas fue la de la verificación de programas , mediante la cual se aplicaron probadores 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, se destacó el Stanford Pascal Verifier desarrollado por David Luckham en la Universidad de Stanford . [17] [18] [19] Este se basaba 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 automática que demostró la capacidad de resolver problemas matemáticos que se anunciaron en los Avisos de la Sociedad Matemática Estadounidense antes de que se publicaran formalmente las soluciones. [ cita requerida ]
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, todavía es semidecidible, y se han desarrollado varios cálculos sólidos y completos que permiten sistemas completamente automatizados. [20] 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. [21] [22]
Existe una superposición sustancial entre los probadores de teoremas automáticos de primer orden y los solucionadores SMT . En general, los probadores de teoremas automáticos se centran en respaldar la lógica de primer orden completa con cuantificadores, mientras que los solucionadores SMT se centran más en respaldar varias teorías (símbolos de predicado interpretados). Los ATP se destacan en problemas con muchos cuantificadores, mientras que los solucionadores SMT funcionan bien en problemas grandes sin cuantificadores. [23] La línea es lo suficientemente borrosa como para que algunos ATP participen en SMT-COMP, mientras que algunos solucionadores SMT participen en CASC . [24]
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 de miles de problemas para demostradores de teoremas (TPTP) [25]) , así como de la Competencia de sistemas CADE ATP (CASC), una competencia anual de sistemas de primer orden para muchas clases importantes de problemas de primer orden.
A continuación se enumeran algunos sistemas importantes (todos han ganado al menos una división de competición CASC).
El Museo de Demostradores de Teoremas [27] es una iniciativa para conservar las fuentes de los sistemas de demostración de teoremas para su análisis futuro, ya que son importantes artefactos culturales y científicos. Contiene las fuentes de muchos de los sistemas mencionados anteriormente.
Los ATP y los solucionadores SMT tienen fortalezas complementarias. Los primeros manejan los cuantificadores de manera más elegante, mientras que los segundos sobresalen en problemas grandes, principalmente de base.
En los últimos años, hemos visto cómo se difuminan las líneas entre SMT-COMP y CASC, con los solucionadores SMT compitiendo en CASC y los ATP compitiendo en SMT-COMP.
para cualquier propósito educativo.