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 la demostración de teoremas matemáticos mediante programas de computadora . El razonamiento automatizado sobre la prueba matemática fue un importante impulso 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 produjo el desarrollo de 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] Sus Fundamentos de la aritmética , publicado en 1884, [2] expresaban (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 lógica formal, abriendo en principio el proceso a la automatización. En 1920, Thoralf Skolem simplificó un resultado anterior 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 la (in)satisfacibilidad de fórmulas de primer orden (y por tanto la validez de un teorema) para reducirse 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 suma 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ó Sobre proposiciones formalmente indecidibles de Principia Mathematica y sistemas relacionados (1931), mostrando que en cualquier sistema axiomático suficientemente fuerte hay enunciados verdaderos que no pueden probarse en el sistema. Este tema fue desarrollado aún más 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 el otro dieron ejemplos concretos de cuestiones indecidibles .
Poco después de la Segunda Guerra Mundial , estuvieron disponibles las primeras computadoras de uso 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 corriendo en un JOHNNIAC, el teórico de la lógica construyó pruebas a partir de un pequeño conjunto de axiomas proposicionales y tres reglas de deducción: modus ponens , sustitución de variables (proposicionales) y sustitución 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 . [7]
El enfoque "heurístico" del teórico de la lógica intentó emular a los matemáticos humanos y no podía garantizar que se pudiera encontrar una prueba para cada teorema válido, ni siquiera en principio. Por el contrario, otros algoritmos más sistemáticos lograron, al menos teóricamente, la integridad de 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 instanciando variables con términos del universo de Herbrand . Luego se podría comprobar la insatisfacibilidad de las fórmulas proposicionales utilizando varios métodos. El programa de Gilmore utilizó la conversión a 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 lógica proposicional , el problema es decidible pero co-NP-completo y, por lo tanto, se cree que sólo 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 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 probarse. Sin embargo, no siempre se pueden reconocer fórmulas inválidas (aquellas que no están implicadas en una teoría determinada).
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 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, mediante 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 todos los enunciados de primer orden sean verdaderos 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 el enunciado que se investiga es indecidible en la teoría que se utiliza, incluso si es verdadero 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 la prueba , donde se certifica que una prueba existente para un teorema es válida. Para esto, 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 demostraciones generadas por los demostradores de teoremas automatizados suelen ser muy grandes, el problema de la compresión de la prueba 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 las pruebas de forma 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 demostración de teoremas si consiste en una demostración tradicional, comenzando con axiomas y produciendo nuevos pasos de inferencia utilizando 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 inteligencia 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 que fueron escritos para demostrar un teorema 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 demostración asistida por máquina del teorema de los cuatro colores , que fue muy controvertida ya que fue la primera demostración matemática reivindicada, que era esencialmente imposible de verificar por humanos debido al enorme tamaño del cálculo del programa (tales demostraciones se llaman no -pruebas encuestables ). Otro ejemplo de prueba asistida por programa es el que muestra que el primer jugador siempre puede ganar el juego de Connect Four .
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 Pentium FDIV , las complicadas unidades de coma flotante de los microprocesadores modernos se han diseñado con especial atención. 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. [12]
Otros usos de los demostradores de teoremas incluyen la síntesis de programas , 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]
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. [ cita necesaria ] Una de las primeras áreas fructíferas fue la de la verificación de programas , mediante la cual se aplicaron demostradores de teoremas de primer orden al problema de verificar la exactitud de los programas de computadora 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 . [15] [16] [17] Esto 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 automatizado que demostró la capacidad de resolver problemas matemáticos que se anunciaron en los Avisos de la Sociedad Estadounidense de Matemáticas antes de que se publicaran formalmente las soluciones. [ cita necesaria ]
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 otra parte, todavía es semidecidible y se han desarrollado una serie de cálculos sólidos y completos que permiten sistemas totalmente automatizados. [18] Las lógicas más expresivas, como la lógica 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. [19] [20]
Existe una superposición sustancial entre los demostradores de teoremas automatizados de primer orden y los solucionadores de SMT . Generalmente, los demostradores de teoremas automatizados se centran en respaldar la lógica completa de primer orden con cuantificadores, mientras que los solucionadores de SMT se centran más en respaldar varias teorías (símbolos de predicados interpretados). Los ATP sobresalen en problemas con muchos cuantificadores, mientras que los solucionadores SMT funcionan bien en problemas grandes sin cuantificadores. [21] La línea es lo suficientemente borrosa como para que algunos ATP participen en SMT-COMP, mientras que algunos solucionadores de SMT participan en CASC . [22]
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) [23]) , así como de la competencia de sistemas CADE ATP (CASC), una competencia anual. competencia 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 competencia CASC).
El Museo de Demostración de Teoremas [25] es una iniciativa para conservar las fuentes de sistemas de demostración de teoremas para análisis futuros, ya que son importantes artefactos culturales/científicos. Tiene las fuentes de muchos de los sistemas mencionados anteriormente.
Los solucionadores de ATP y SMT tienen fortalezas complementarias.
Los primeros manejan los cuantificadores con mayor elegancia, mientras que los segundos destacan en problemas grandes, en su mayoría básicos.
En los últimos años, hemos visto una línea borrosa entre SMT-COMP y CASC con solucionadores de SMT compitiendo en CASC y ATP compitiendo en SMT-COMP.
Este material puede reproducirse con cualquier fin educativo,...