Demostración automática de teoremas

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. por programas de computadora. El razonamiento automatizado sobre la prueba matemática fue un gran impulso para el desarrollo de la informática.

Fundamentos lógicos

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 de Frege (1879) introdujo tanto un cálculo proposicional completo como lo que es esencialmente la lógica moderna de predicados. Su Fundamentos de aritmética, publicado en 1884, 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, y con una segunda edición revisada en 1927. Russell y Whitehead pensaron que podían derivar toda la verdad matemática usando axiomas e inferencias. reglas de la 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 las fórmulas de primer orden (y por lo tanto la validez de un teorema) para reducirse a (potencialmente infinitos) problemas de satisfacibilidad proposicional.

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. 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 lo suficientemente fuerte hay proposiciones verdaderas que no pueden probarse en el sistema. Este tema fue desarrollado 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 para preguntas indecidibles.

Primeras implementaciones

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 probar que la suma de dos números pares es par'. Más ambicioso fue 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 J. C. 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.

La "heurística" El enfoque de la máquina de la teoría lógica trató de emular a los matemáticos humanos y no pudo garantizar que se pudiera encontrar una demostración 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.

Decidibilidad del problema

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 frecuente de 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 comprobables) son exactamente las fórmulas bien formadas lógicamente válidas, por lo que identificar fórmulas válidas es recursivamente enumerable: dados recursos ilimitados, cualquier fórmula válida puede eventualmente ser probado. Sin embargo, las fórmulas inválidas (aquellas que no están implícitas en una teoría dada), no siempre pueden ser reconocidas.

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 cuyos axiomas propios sean verdaderos para los números naturales no puede demostrar que todos los enunciados de primer orden son verdaderos para los números naturales, incluso si se permite que la lista de axiomas propios sea infinita. enumerable. De ello se deduce que un probador automático de teoremas no terminará mientras busca una prueba precisamente cuando el enunciado que se investiga es indecidible en la teoría que se usa, incluso si es verdadero en el modelo de interés. A pesar de este límite teórico, en la práctica, los probadores 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).

Problemas relacionados

Un problema más simple, pero relacionado, es la verificación de 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 ser verificado por una función o programa recursivo primitivo y, por lo tanto, el problema siempre es decidible.

Dado que las pruebas generadas por los probadores 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 probador sea más pequeña y, en consecuencia, más fácilmente comprensible y verificable.

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, donde el usuario proporciona la prueba de manera formal, o se pueden realizar automáticamente tareas de prueba significativas. Los probadores interactivos se utilizan para una variedad de tareas, pero incluso los sistemas totalmente automáticos han demostrado una serie de teoremas difíciles e interesantes, incluido al menos uno que ha eludido a los matemáticos humanos durante mucho tiempo, a saber, la conjetura de Robbins. 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 consta de una demostración tradicional, que comienza con axiomas y produce 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 de 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 probar un teorema en particular, con una prueba (generalmente informal) de que si el programa termina con cierto resultado, 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 ya que la primera prueba matemática reivindicada que era esencialmente imposible de verificar por humanos debido al enorme tamaño del cálculo del programa (como las pruebas se llaman pruebas no encuestables). Otro ejemplo de demostración asistida por programa es el que muestra que el primer jugador siempre puede ganar el juego Connect Four.

Usos industriales

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 Pentium FDIV, las complicadas unidades de punto flotante de los microprocesadores modernos se han diseñado con un escrutinio adicional. AMD, Intel y otros utilizan teoremas automatizados para verificar que la división y otras operaciones se implementen correctamente en sus procesadores.

Demostración del teorema de primer orden

A fines de la década de 1960, las agencias que financiaban la investigación en deducción automática comenzaron a enfatizar la necesidad de aplicaciones prácticas. 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 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. Esto se basó en 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 Matemática Estadounidense 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 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 totalmente automatizados. 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.

Puntos de referencia, competencias y fuentes

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 probadores de teoremas (TPTP), así como de la Competencia del sistema CADE ATP (CASC), un evento anual competencia de los sistemas de primer orden para muchas clases importantes de problemas de primer orden.

Algunos sistemas importantes (todos han ganado al menos una división de competencia CASC) se enumeran a continuación.

• E es un probador de alto rendimiento para la lógica de primer orden completo, pero construido sobre un cálculo puramente ecual, desarrollado originalmente en el grupo de razonamiento automatizado de la Universidad Técnica de Munich 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 de Argonne, se basa en la resolución y paramodulación de primer orden. Otter ha sido reemplazado por Prover9, que está emparejado con Mace4.
• SETHEO es un sistema de alto rendimiento basado en el cálculo de eliminación modelo dirigido por objetivos, desarrollado originalmente por un equipo bajo la dirección de Wolfgang Bibel. E y SETHEO se han combinado (con otros sistemas) en el probador de teorema compuesto E-SETHEO.
• Vampire fue desarrollado e implementado originalmente en la Universidad de Manchester por Andrei Voronkov y Krystof Hoder. Ahora es desarrollado por un creciente equipo internacional. Ha ganado la división FOF (entre otras divisiones) en el Concurso del Sistema CADE ATP regularmente desde 2001.
• Waldmeister es un sistema especializado para la lógica de primera orden unitaria desarrollada por Arnim Buch y Thomas Hillenbrand. Ganó la división CASC UEQ durante catorce años consecutivos (1997–2010).
• SPASS es un probador de teorema lógico de primer orden con igualdad. Esto es desarrollado por el grupo de investigación Automation of Logic, Max Planck Institute for Computer Science.

El Theorem Prover Museum es una iniciativa para conservar las fuentes de los sistemas de demostración de teoremas para futuros análisis, ya que son importantes artefactos culturales/científicos. Tiene las fuentes de muchos de los sistemas mencionados anteriormente.

Técnicas populares

• Resolución de primera orden con unificación
• Eliminación modelo
• Método de tablas analíticas
• Superposición y reescritura del término
• Verificación de modelos
• Inducción matemática
• Diagramas de decisión binarios
• DPLL
• Unificación de orden superior

Sistemas de software

Software libre

• Alt-Ergo
• Automatismo
• CVC
• E
• GKC
• Gödel machine
• iProver
• IsaPlanner
• KED teorem prover
• leanCoP
• Leo II
• LCF
• Logictools online theorem prover
• LoTREC
• MetaPRL
• Mizarra
• NuPRL
• Paradox
• Prover9
• PVS
• Simplificar
• SPARK (lengua de programación)
• Doce.
• Z3 Theorem Prover

Software propietario

• Acumen RuleManager (producto comercial)
• ALLIGATOR (CC BY-NC-SA 2.0 UK)
• CARINE
• KIV (gratuitamente disponible como plugin para Eclipse)
• Prover Plug-In (producto del motor de prueba comercial)
• ProverBox
• Wolfram Mathematica
• ResearchCyc
• Spear modular aritmmetic theorem prover