La demostración automática de teoremas (también conocida como ATP o deducción automática ) es un subcampo del razonamiento automatizado y la lógica matemática que se ocupa de demostrar teoremas matemáticos mediante programas de computadora . El razonamiento automatizado sobre la prueba matemática fue un gran impulso para el desarrollo de la informática .
Si bien las raíces de la lógica formalizada se remontan a Aristóteles , el final del siglo XIX y principios del XX vio el desarrollo de la lógica moderna y las matemáticas formalizadas. El Begriffsschrift de Frege (1879) introdujo tanto un cálculo proposicional completo como lo que es esencialmente la lógica moderna de predicados . [1] Su Fundamentos de la 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 usando axiomas y reglas de inferencia de lógica formal, en principio abriendo 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 las fórmulas de primer orden (y por lo 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 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 idioma era verdadera o falsa. [6] [7] Sin embargo, poco después de este resultado positivo, Kurt Gödel publicó On Formally Undecidible Propositions of Principia Mathematica and Related Systems (1931), mostrando que en cualquier sistema axiomático suficientemente fuerte hay proposiciones verdaderas que no pueden probarse en el sistema. . Este tema fue desarrollado aún más en la década de 1930 por Alonzo Church yAlan Turing , quien por un lado dio dos definiciones independientes pero equivalentes de computabilidad , y por otro dio ejemplos concretos para 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 en 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 Theory Machine 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, la Máquina de Teoría 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 el reemplazo de fórmulas por su definición. El sistema utilizó orientación heurística y logró probar 38 de los primeros 52 teoremas de los Principia . [7]
El enfoque "heurístico" de Logic Theory Machine intentó emular a los matemáticos humanos y no pudo garantizar que se pudiera encontrar una prueba para cada teorema válido, incluso 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, las fórmulas proposicionales podrían verificarse por insatisfacibilidad 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]