Herramienta de software para ayudar con el desarrollo de pruebas formales mediante la colaboración hombre-máquina
Una sesión de prueba interactiva en CoqIDE, que muestra el script de prueba a la izquierda y el estado de la prueba a la derecha.
En informática y lógica matemática , un asistente de prueba o demostrador de teoremas interactivo es una herramienta de software para ayudar con el desarrollo de pruebas formales mediante la colaboración hombre-máquina. Se trata de algún tipo de editor de pruebas interactivo, u otra interfaz , con la que un humano puede guiar la búsqueda de pruebas, cuyos detalles se almacenan en una computadora y algunos pasos son proporcionados por ella .
Un esfuerzo reciente dentro de este campo está haciendo que estas herramientas utilicen inteligencia artificial para automatizar la formalización de las matemáticas ordinarias. [1]
Comparación de sistemas
ACL2 : un lenguaje de programación, una teoría lógica de primer orden y un demostrador de teoremas (con modos interactivo y automático) en la tradición de Boyer-Moore.
Coq : permite la expresión de afirmaciones matemáticas, verifica mecánicamente las pruebas de estas afirmaciones, ayuda a encontrar pruebas formales y extrae un programa certificado a partir de la prueba constructiva de su especificación formal.
Demostradores del teorema HOL : una familia de herramientas derivadas en última instancia del demostrador del teorema LCF . En estos sistemas, el núcleo lógico es una biblioteca de su lenguaje de programación. Los teoremas representan nuevos elementos del lenguaje y sólo pueden introducirse mediante "estrategias" que garanticen la corrección lógica. La composición de estrategias brinda a los usuarios la capacidad de producir pruebas importantes con relativamente pocas interacciones con el sistema. Los miembros de la familia incluyen:
HOL4 – El "descendiente primario", aún en desarrollo activo. Soporte tanto para Moscú ML como para Poly/ML . Tiene una licencia estilo BSD .
HOL Light : una próspera "bifurcación minimalista". Basado en OCaml .
ProofPower: pasó a ser propietario y luego volvió al código abierto. Basado en ML estándar .
IMPS, un sistema interactivo de prueba matemática. [8]
Isabelle es un demostrador de teoremas interactivo, sucesor de HOL. El código base principal tiene licencia BSD, pero la distribución Isabelle incluye muchas herramientas complementarias con diferentes licencias.
TPS y ETPS: demostradores de teoremas interactivos también basados en cálculo lambda de tipo simple, pero basados en una formulación independiente de la teoría lógica y una implementación independiente.
Interfaces de usuario
Una interfaz popular para asistentes de pruebas es Proof General, basada en Emacs y desarrollada en la Universidad de Edimburgo .
Coq incluye CoqIDE, que está basado en OCaml/ Gtk . Isabelle incluye Isabelle/jEdit, que se basa en jEdit y la infraestructura Isabelle/ Scala para el procesamiento de pruebas orientado a documentos. Más recientemente, las extensiones de Visual Studio Code han sido desarrolladas para Coq, [9] Isabelle por Makarius Wenzel, [10] y para Lean 4 por los desarrolladores de leanprover. [11]
Grado de formalización
Freek Wiedijk ha elaborado una clasificación de los asistentes de demostración según la cantidad de teoremas formalizados de una lista de 100 teoremas conocidos. En septiembre de 2023, solo cinco sistemas han formalizado demostraciones de más del 70% de los teoremas: Isabelle, HOL Light, Coq, Lean y Metamath. [12] [13]
Pruebas formalizadas notables
La siguiente es una lista de pruebas notables que se han formalizado en los asistentes de prueba.
^ Ornes, Stephen (27 de agosto de 2020). "Revista Quanta: ¿Qué tan cerca están las computadoras de automatizar el razonamiento matemático?".
^ Caza, Warren; Matt Kaufmann; Robert Belarmino Krug; J Moore; Eric W. Smith (2005). "Metarazonamiento en ACL2" (PDF) . Demostración de teoremas en lógica de orden superior . Apuntes de conferencias sobre informática. vol. 3603, págs. 163-178. doi :10.1007/11541868_11. ISBN978-3-540-28372-0.
^ abc "agda/agda: Agda es un lenguaje de programación escrito de forma dependiente/demostración de teoremas interactivo". GitHub . Consultado el 31 de julio de 2024 .
^ "La Wiki de Agda" . Consultado el 31 de julio de 2024 .
^ Busque "pruebas por reflexión": arXiv :1803.06547
^ "Página de lanzamientos de Lean 4". GitHub . Consultado el 15 de octubre de 2023 .
^ Granjero, William M.; Guttman, Josué D.; Thayer, F.Javier (1993). "IMPS: un sistema de prueba matemático interactivo". Revista de razonamiento automatizado . 11 (2): 213–248. doi :10.1007/BF00881906. S2CID 3084322 . Consultado el 22 de enero de 2020 .
^ "coq-comunidad/vscoq". 29 de julio de 2024 – vía GitHub.
^ Wenzel, Makario. "Isabel" . Consultado el 2 de noviembre de 2019 .
^ "Código VS Lean 4". GitHub . Consultado el 15 de octubre de 2023 .
^ Wiedijk, Freek (15 de septiembre de 2023). "Formalizando 100 teoremas".
^ Geuvers, Herman (febrero de 2009). "Asistentes de prueba: Historia, ideas y futuro". Sadhana . 34 (1): 3–25. doi : 10.1007/s12046-009-0001-5 . hdl : 2066/75958 . S2CID 14827467.
^ "Feit Thomson demostró en coq - Centro conjunto de investigación de Microsoft Inria". 2016-11-19. Archivado desde el original el 19 de noviembre de 2016 . Consultado el 7 de diciembre de 2023 .
^ Licata, Daniel R.; Shulman, Michael (2013). "Cálculo del grupo fundamental del círculo en la teoría de tipos de homotopía". 2013 28º Simposio anual ACM/IEEE sobre lógica en informática. págs. 223-232. arXiv : 1301.3443 . doi :10.1109/lics.2013.28. ISBN978-1-4799-0413-6. S2CID 5661377 . Consultado el 7 de diciembre de 2023 .
^ "El problema matemático que lleva 3500 años en desarrollo finalmente tiene una solución". IFLSiencia . 2022-03-11 . Consultado el 9 de febrero de 2024 .
^ Avigad, Jeremy (2023). "Matemáticas y el giro formal". arXiv : 2311.00007 [matemáticas.HO].
^ Sloman, Leila (6 de diciembre de 2023). "'A-Team' of Math demuestra un vínculo fundamental entre la suma y los conjuntos" . Revista Quanta . Consultado el 7 de diciembre de 2023 .
^ "Hemos demostrado" BB(5) = 47.176.870"". El desafío del castor ocupado . 2024-07-02 . Consultado el 9 de julio de 2024 .
Referencias
Barendregt, Henk ; Geuvers, Herman (2001). "18. Asistentes de prueba que utilizan sistemas de tipos dependientes" (PDF) . En Robinson, Alan JA; Voronkov, Andrei (eds.). Manual de razonamiento automatizado . vol. 2. Elsevier. págs. 1149–. ISBN 978-0-444-50812-6. Archivado desde el original (PDF) el 27 de julio de 2007.
Pfenning, Frank (1996). "La práctica de los marcos lógicos". En Kirchner, H. (ed.). Árboles en Álgebra y Programación - CAAP '96 . Apuntes de conferencias sobre informática. vol. 1059. Saltador. págs. 119-134. doi :10.1007/3-540-61064-2_33. ISBN 3-540-61064-2.
Condestable, Robert L. (1998). "X. Tipos en informática, filosofía y lógica". En Buss, SR (ed.). Manual de teoría de la prueba . Estudios de Lógica. vol. 137. Elsevier. págs. 683–786. ISBN 978-0-08-053318-6.
Wiedijk, Freek (2005). "Los diecisiete probadores del mundo" (PDF) . Universidad Radboud de Nimega.
Enlaces externos
Museo del demostrador de teoremas
"Introducción" a la Programación Certificada con Tipos Dependientes .
Introducción al Asistente de prueba Coq (con una introducción general a la demostración interactiva de teoremas)
Demostración interactiva de teoremas para usuarios de Agda
Una lista de herramientas para demostrar teoremas
Catálogos
Matemáticas digitales por categoría: probadores de tácticas
Sistemas y grupos de deducción automatizados
Demostración de teoremas y sistemas de razonamiento automatizados
Base de datos de sistemas de razonamiento mecanizado existentes
NuPRL: Otros Sistemas
"Marcos Lógicos Específicos e Implementaciones". Archivado desde el original el 10 de abril de 2022 . Consultado el 15 de febrero de 2024 .(Por Frank Pfenning).