Herramienta de software para ayudar en el desarrollo de pruebas formales mediante la colaboración hombre-máquina
En informática y lógica matemática , un asistente de pruebas o demostrador interactivo de teoremas es una herramienta de software que ayuda a desarrollar pruebas formales mediante la colaboración entre humanos y máquinas. Esto implica 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 es hacer 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 interactivos y automáticos) 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 de la prueba constructiva de su especificación formal.
Demostradores de teoremas HOL : una familia de herramientas derivadas en última instancia del demostrador de teoremas LCF . En estos sistemas, el núcleo lógico es una biblioteca de su lenguaje de programación. Los teoremas representan elementos nuevos del lenguaje y solo se pueden introducir mediante "estrategias" que garantizan la corrección lógica. La composición de estrategias brinda a los usuarios la capacidad de producir demostraciones significativas con relativamente pocas interacciones con el sistema. Los miembros de la familia incluyen:
HOL Light : una "bifurcación minimalista" en auge, basada en OCaml .
ProofPower: pasó a ser propietario y luego volvió a ser de código abierto. Basado en Standard ML .
IMPS, un sistema interactivo de pruebas matemáticas. [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 tipos simples, 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 los asistentes de prueba es Proof General, basado en Emacs , desarrollado en la Universidad de Edimburgo .
Coq incluye CoqIDE, que se basa 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, se han desarrollado extensiones de Visual Studio Code para Coq, [9] Isabelle por Makarius Wenzel, [10] y para Lean 4 por los desarrolladores de leanprover. [11]
Alcance de la formalización
Freek Wiedijk ha estado llevando un ranking de asistentes de demostración según la cantidad de teoremas formalizados de una lista de 100 teoremas conocidos. A septiembre de 2023, solo cinco sistemas han formalizado demostraciones de más del 70% de los teoremas, a saber, Isabelle, HOL Light, Coq, Lean y Metamath. [12] [13]
Pruebas formalizadas notables
La siguiente es una lista de pruebas notables que se han formalizado dentro de los asistentes de prueba.
^ Ornes, Stephen (27 de agosto de 2020). "Quanta Magazine – ¿Qué tan cerca están las computadoras de automatizar el razonamiento matemático?".
^ Hunt, Warren; Matt Kaufmann; Robert Bellarmine Krug; J Moore; Eric W. Smith (2005). "Meta Reasoning in ACL2" (PDF) . Demostración de teoremas en lógica de orden superior . Apuntes de clase en 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 de tipado dependiente / demostrador interactivo de teoremas". GitHub . Consultado el 31 de julio de 2024 .
^ "La Wiki de Agda" . Consultado el 31 de julio de 2024 .
^ Buscar "pruebas por reflexión": arXiv :1803.06547
^ "Página de lanzamientos de Lean 4". GitHub . Consultado el 15 de octubre de 2023 .
^ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier (1993). "IMPS: Un sistema interactivo de prueba matemática". Journal of Automated Reasoning . 11 (2): 213–248. doi :10.1007/BF00881906. S2CID 3084322 . Consultado el 22 de enero de 2020 .
^ "coq-community/vscoq". 29 de julio de 2024 – vía GitHub.
^ Wenzel, Makarius. "Isabelle" . Consultado el 2 de noviembre de 2019 .
^ "VS Code 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". Sādhanā . 34 (1): 3–25. doi : 10.1007/s12046-009-0001-5 . hdl : 2066/75958 . S2CID 14827467.
^ "Feit Thomson demostró en Coq - Microsoft Research Inria Joint Centre". 19 de noviembre de 2016. 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". 28.° Simposio anual ACM/IEEE sobre lógica en informática de 2013. 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 .
^ "Un problema matemático que se ha estado desarrollando durante 3500 años finalmente obtiene una solución". IFLScience . 2022-03-11 . Consultado el 2024-02-09 .
^ Avigad, Jeremy (2023). "Matemáticas y el giro formal". arXiv : 2311.00007 [math.HO].
^ Sloman, Leila (6 de diciembre de 2023). "El 'Equipo A' de matemáticas demuestra un vínculo crítico entre la suma y los conjuntos". Revista Quanta . Consultado el 7 de diciembre de 2023 .
^ "Hemos demostrado que "BB(5) = 47.176.870"". El desafío del castor atareado . 2024-07-02 . Consultado el 2024-07-09 .
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 clase en informática. Vol. 1059. Springer. págs. 119–134. doi :10.1007/3-540-61064-2_33. ISBN .3-540-61064-2.
Constable, 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 de Demostradores de Teoremas
"Introducción" a la Programación Certificada con Tipos Dependientes .
Introducción al Asistente de demostración 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: Demostradores de tácticas
Sistemas y grupos de deducción automática
Sistemas de demostración de teoremas y razonamiento automático
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).