La demostración automatizada 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 la demostración de teoremas matemáticos mediante programas informáticos . El razonamiento automatizado sobre la demostración 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. La Begriffsschrift de Frege (1879) 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 , publicados en 1884, [2] expresaron (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 en 1910-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, abriendo en principio el proceso a la automatización. En 1920, Thoralf Skolem simplificó un resultado anterior de Leopold Löwenheim , lo que llevó al teorema de Löwenheim-Skolem y, en 1930, a la noción de un universo Herbrand y una interpretación Herbrand que permitía (in) satisfacibilidad de 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 dio 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 Undecidable Propositions of Principia Mathematica and Related Systems (1931), mostrando que en cualquier sistema axiomático suficientemente fuerte hay afirmaciones verdaderas que no pueden ser probadas 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 para preguntas indecidibles.
Primeras implementaciones
Poco después de la Segunda Guerra Mundial , las primeras computadoras de propósito general estuvieron disponibles. 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 . 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ó 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ó orientación heurística y logró demostrar 38 de los primeros 52 teoremas de los Principia . [7]
El enfoque "heurístico" de la máquina de teoría lógica trató de emular a los matemáticos humanos y no pudo garantizar que se pudiera encontrar una prueba para cada teorema válido, incluso en principio. En contraste, otros algoritmos más sistemáticos lograron, al menos teóricamente, la completitud 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 . A continuación, se podría comprobar la insatisfacción 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. [7] [9]
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 demostrables) son exactamente las fórmulas lógicamente válidas bien formadas , por lo que identificar fórmulas válidas es recursivamente enumerable : dados recursos ilimitados, cualquier fórmula válida puede eventualmente ser probada. 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, según el teorema de incompletitud de Gödel , sabemos que cualquier teoría cuyos axiomas propios 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 propios sea infinitamente enumerable. De ello se deduce que un demostrador de teoremas automatizado no terminará mientras busca una prueba precisamente cuando el enunciado que se investiga es indecidible en la teoría que se está utilizando, incluso si es cierto 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 pruebas , donde una prueba existente de un teorema se certifica como 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 demostraciones generadas por los probadores 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 probador sea más pequeña y, en consecuencia, más fácilmente comprensible y comprobable.
Los asistentes de pruebas requieren que un usuario humano dé pistas al sistema. Dependiendo del grado de automatización, el probador se puede reducir esencialmente a un verificador de pruebas, y el usuario proporciona la prueba de una 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 demostración tradicional, comenzando con axiomas y produciendo nuevos pasos de inferencia usando 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 prueba de teoremas que utilizan la verificación de modelos como regla de inferencia. También hay programas que fueron escritos para probar un teorema en particular, con una prueba (generalmente informal) de que si el programa termina con un 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 los humanos debido al enorme tamaño del cálculo del programa (tales demostraciones se denominan 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 .
Usos industriales
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 punto flotante de los microprocesadores modernos se han diseñado con un escrutinio adicional. AMD , Intel y otros utilizan un teorema automatizado que demuestra que la división y otras operaciones se implementan 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 los probadores de teoremas de primer orden se aplicaron 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 . Esto se basa en la resolución de Stanford PRVADR también desarrollado en Stanford usando John Alan Robinson 's resolución principio. 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 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, sigue siendo semidecidible y se han desarrollado una serie de cálculos sólidos y completos que permiten sistemas totalmente automatizados. [12] 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. [13] [14]
Benchmarks, concursos 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) [15] , así como de la Competencia de sistemas CADE ATP (CASC), una 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 completa de primer orden, 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 de Argonne , se basa en una resolución y paramodulación de primer orden . Desde entonces, 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 de modelos dirigido a objetivos , desarrollado originalmente por un equipo bajo la dirección de 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 Krystof Hoder. Ahora es desarrollado por un equipo internacional en crecimiento. Ha ganado la división FOF (entre otras divisiones) en la Competencia del Sistema CADE ATP regularmente desde 2001.
- Waldmeister es un sistema especializado para la lógica de primer orden de ecuaciones unitarias desarrollado por Arnim Buch y Thomas Hillenbrand. Ganó la división CASC UEQ durante catorce años consecutivos (1997-2010).
- SPASS es un demostrador de teoremas lógicos de primer orden con igualdad. Este es desarrollado por el grupo de investigación Automatización de la Lógica, Instituto Max Planck de Ciencias de la Computación .
El Museo de Probadores de Teoremas es una iniciativa para conservar las fuentes de los sistemas de probadores de teoremas para análisis futuros, ya que son importantes artefactos culturales / científicos. Tiene las fuentes de muchos de los sistemas mencionados anteriormente.
Técnicas populares
- Resolución de primer orden con unificación
- Eliminación de modelos
- Método de cuadros analíticos
- Superposición y reescritura de términos
- Comprobación de modelo
- Inducción matemática [16]
- Diagramas de decisión binarios
- DPLL
- Unificación de orden superior
Sistemas de software
Nombre | Tipo de licencia | servicio web | Biblioteca | Ser único | Última actualización ( formato AAAA-mm-dd ) |
---|---|---|---|---|---|
ACL2 | BSD de 3 cláusulas | No | No | sí | Mayo de 2019 |
Prover9 / Nutria | Dominio publico | A través del sistema en TPTP | sí | No | 2009 |
Broma | GPLv2 | sí | sí | No | 15 de mayo de 2015 |
PVS | GPLv2 | No | sí | No | 14 de enero de 2013 |
Leo II | Licencia BSD | A través del sistema en TPTP | sí | sí | 2013 |
EQP | ? | No | sí | No | Mayo de 2009 |
TRISTE | GPLv3 | sí | sí | No | 27 de agosto de 2008 |
PhoX | ? | No | sí | No | 28 de septiembre de 2017 |
KeYmaera | GPL | A través de Java Webstart | sí | sí | 11 de marzo de 2015 |
Gandalf | ? | No | sí | No | 2009 |
mi | GPL | A través del sistema en TPTP | No | sí | 4 de julio de 2017 |
SNARK | Licencia pública de Mozilla 1.1 | No | sí | No | 2012 |
Vampiro | Licencia de vampiro | A través del sistema en TPTP | sí | sí | 14 de diciembre de 2017 |
Sistema de prueba de teoremas (TPS) | Acuerdo de distribución de TPS | No | sí | No | 4 de febrero de 2012 |
SPASS | Licencia FreeBSD | sí | sí | sí | Noviembre de 2005 |
IsaPlanner | GPL | No | sí | sí | 2007 |
Clave | GPL | sí | sí | sí | 11 de octubre de 2017 |
princesa | lgpl v2.1 | A través de Java Webstart y System en TPTP | sí | sí | 27 de enero de 2018 |
iProver | GPL | A través del sistema en TPTP | No | sí | 2018 |
Metateorema | Freeware | No | No | sí | Abril de 2020 |
Demostrador del teorema Z3 | Licencia MIT | sí | sí | sí | 19 de noviembre de 2019 |
Software libre
- Alt-Ergo
- Automath
- CVC
- mi
- GKC
- Máquina de Gödel
- iProver
- IsaPlanner
- Demostrador del teorema KED [17]
- leanCoP [18]
- Leo II
- LCF
- Aplicación de navegador Logictools
- LoTREC [19]
- MetaPRL [20]
- Mizar
- NuPRL
- Paradoja
- Prover9
- Simplificar
- SPARK (lenguaje de programación)
- Duodécimo
- Demostrador del teorema Z3
Software propietario
- Acumen RuleManager (producto comercial)
- ALLIGATOR (CC BY-NC-SA 2.0 Reino Unido)
- CARINE
- KIV (disponible gratuitamente como complemento para Eclipse )
- Prover Plug-In (producto de motor de prueba comercial)
- ProverBox
- Wolfram Mathematica [21]
- ResearchCyc
- Demostrador del teorema aritmético modular de Spear
Ver también
- Correspondencia Curry-Howard
- Computación simbólica
- Prueba asistida por computadora
- Verificación formal
- Programación lógica
- Comprobación de pruebas
- Comprobación de modelo
- Prueba de complejidad
- Sistema de álgebra informática
- Análisis de programas (informática)
- Solucionador de problemas generales
- Lenguaje metamath para matemáticas formalizadas
Notas
- ^ Frege, Gottlob (1879). Begriffsschrift . Verlag Louis Neuert.
- ^ Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF) . Breslau: Wilhelm Kobner. Archivado desde el original (PDF) el 26 de septiembre de 2007 . Consultado el 2 de septiembre de 2012 .
- ^ Bertrand Russell; Alfred North Whitehead (1910-1913). Principia Mathematica (1ª ed.). Prensa de la Universidad de Cambridge.
- ^ Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica (2ª ed.). Prensa de la Universidad de Cambridge.
- ^ Herbrand, Jaques (1930). Recherches sur la théorie de la démonstration .
- ^ Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves . Warszawa: 92–101.
- ^ a b c d Davis, Martin (2001), "La historia temprana de la deducción automatizada" , en Robinson, Alan ; Voronkov, Andrei (eds.), Manual de razonamiento automatizado , 1 , Elsevier)
- ^ Bibel, Wolfgang (2007). "Historia temprana y perspectivas de la deducción automatizada" (PDF) . Ki 2007 . LNAI. Springer (4667): 2–18 . Consultado el 2 de septiembre de 2012 .
- ^ Gilmore, Paul (1960). "Un procedimiento de prueba para la teoría de la cuantificación: su justificación y realización". Revista de investigación y desarrollo de IBM . 4 : 28–35. doi : 10.1147 / rd.41.0028 .
- ^ WW McCune (1997). "Solución del problema de Robbins". Revista de razonamiento automatizado . 19 (3): 263-276. doi : 10.1023 / A: 1005843212881 . S2CID 30847540 .
- ^ Gina Kolata (10 de diciembre de 1996). "Prueba matemática informática muestra poder de razonamiento" . The New York Times . Consultado el 11 de octubre de 2008 .
- ^ Loveland, DW (1986). "Demostración automatizada de teoremas: mapeo de lógica en AI" . Actas del Simposio Internacional ACM SIGART sobre Metodologías para Sistemas Inteligentes . Knoxville, Tennessee, Estados Unidos: ACM Press: 224. doi : 10.1145 / 12808.12833 . ISBN 978-0-89791-206-8. S2CID 14361631 .
- ^ Kerber, Manfred. " Cómo demostrar teoremas de orden superior en lógica de primer orden ". (1999).
- ^ Benzmüller, Christoph y col. " LEO-II: un demostrador automático de teoremas cooperativo para la lógica clásica de orden superior (descripción del sistema) ". Conferencia conjunta internacional sobre razonamiento automatizado. Springer, Berlín, Heidelberg, 2008.
- ^ Sutcliffe, Geoff. "La biblioteca de problemas de TPTP para la demostración automatizada de teoremas" . Consultado el 15 de julio de 2019 .
- ^ Bundy, Alan. La automatización de la prueba por inducción matemática . 1999.
- ^ Artosi, Alberto, Paola Cattabriga y Guido Governatori. " Ked: un demostrador de teoremas deónticos ". XI Congreso Internacional de Programación Lógica (ICLP'94). 1994.
- ^ Otten, Jens; Bibel, Wolfgang (2003). "LeanCoP: demostración del teorema basado en conexión Lean" . Revista de Computación Simbólica . 36 (1-2): 139-161. doi : 10.1016 / S0747-7171 (03) 00037-3 .
- ^ Del Cerro, Luis Fariñas; Fauthoux, David; Gasquet, Olivier; Herzig, Andreas; Longin, Dominique; Massacci, Fabio (2001). "Lotrec: el genérico de prueba de Tableau para lógica modal y descriptiva". Razonamiento automatizado . Apuntes de conferencias en Ciencias de la Computación. 2083 . págs. 453–458. doi : 10.1007 / 3-540-45744-5_38 . ISBN 978-3-540-42254-9.
- ^ Hickey, Jason y col. " MetaPRL: un entorno lógico modular ". Conferencia internacional sobre demostración de teoremas en lógicas de orden superior. Springer, Berlín, Heidelberg, 2003.
- ^ [1] Documentación de Mathematica
Referencias
- Chin-Liang Chang; Richard Char-Tung Lee (1973). Demostración de teoremas mecánicos y lógicos simbólicos . Prensa académica .
- Loveland, Donald W. (1978). Demostración automatizada de teoremas: una base lógica. Estudios Fundamentales en Ciencias de la Computación Volumen 6 . Editorial de Holanda Septentrional .
- Luckham, David (1990). Programación con especificaciones: una introducción a Anna, un lenguaje para especificar programas Ada . Textos y monografías de Springer-Verlag en informática, 421 págs. ISBN 978-1461396871.
- Gallier, Jean H. (1986). Lógica para la informática: fundamentos de la demostración automática de teoremas . Harper & Row Publishers (disponible para descarga gratuita).
- Duffy, David A. (1991). Principios de la demostración automatizada de teoremas . John Wiley e hijos .
- Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992). Razonamiento automatizado: Introducción y aplicaciones (2ª ed.). McGraw – Hill .
- Alan Robinson; Andrei Voronkov, eds. (2001). Manual de Razonamiento Automatizado Volumen I y II . Elsevier y MIT Press .
- Adecuado, Melvin (1996). Lógica de primer orden y demostración automatizada de teoremas (2ª ed.). Springer .
enlaces externos
- Una lista de herramientas para demostrar teoremas