Asistente de pruebas

Herramienta de software para ayudar en 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 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:
  • HOL4  : el "descendiente primario", aún en desarrollo activo. Admite tanto Moscow ML como Poly/ML . Tiene una licencia de estilo BSD .
  • 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.
• Jape  – Basado en Java.
• Inclinarse
• LEGO
• Matita  – Un sistema ligero basado en el Cálculo de Construcciones Inductivas.
• MINLOG  – Un asistente de prueba basado en lógica mínima de primer orden.
• Mizar  – Un asistente de pruebas basado en lógica de primer orden, en un estilo de deducción natural , y en la teoría de conjuntos de Tarski-Grothendieck .
• PhoX  – Un asistente de pruebas basado en lógica de orden superior y extensible.
• Sistema de verificación de prototipos (PVS): un lenguaje y sistema de prueba basado en lógica de orden superior.
• 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.

Véase también

• Demostración automática de teoremas  : subcampo del razonamiento automático y la lógica matemática
• Prueba asistida por computadora  : prueba matemática generada al menos parcialmente por computadora.
• Verificación formal  : comprobar o refutar la exactitud de ciertos algoritmos previstos
• Manifiesto QED  – Propuesta para una base de datos informática de todo el conocimiento matemático
• Teorías de satisfacibilidad módulo  – Problema lógico estudiado en informática
• Prover9 – es un demostrador de teoremas automatizado para lógica ecuacional y de primer orden

Notas

1. Ornes, Stephen (27 de agosto de 2020). "Quanta Magazine – ¿Qué tan cerca están las computadoras de automatizar el razonamiento matemático?".
2. 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. ISBN 978-3-540-28372-0.
3. "agda/agda: Agda es un lenguaje de programación de tipado dependiente / demostrador interactivo de teoremas". GitHub . Consultado el 31 de julio de 2024 .
4. "La Wiki de Agda" . Consultado el 31 de julio de 2024 .
5. Buscar "pruebas por reflexión": arXiv :1803.06547
6. "Página de lanzamientos de Lean 4". GitHub . Consultado el 15 de octubre de 2023 .
7. "Versión v0.198 · ​​metamath/Metamath-exe". GitHub .
8. 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 .
9. "coq-community/vscoq". 29 de julio de 2024 – vía GitHub.
10. Wenzel, Makarius. "Isabelle" . Consultado el 2 de noviembre de 2019 .
11. "VS Code Lean 4". GitHub . Consultado el 15 de octubre de 2023 .
12. Wiedijk, Freek (15 de septiembre de 2023). "Formalizando 100 teoremas".
13. 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.
14. Gonthier, Georges (2008), "Demostración formal: el teorema de los cuatro colores" (PDF) , Notices of the American Mathematical Society , 55 (11): 1382–1393, MR  2463991, archivado (PDF) desde el original el 2011-08-05
15. "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 .
16. 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. ISBN 978-1-4799-0413-6. S2CID  5661377 . Consultado el 7 de diciembre de 2023 .
17. "Un problema matemático que se ha estado gestando durante 3500 años finalmente obtiene una solución". IFLScience . 2022-03-11 . Consultado el 2024-02-09 .
18. Avigad, Jeremy (2023). "Matemáticas y el giro formal". arXiv : 2311.00007 [math.HO].
19. 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 .
20. "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 . "17. Marcos lógicos" (PDF) . Manual vol 2 2001 . págs. 1065–1148.
• 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).
• DMOZ : Ciencias: Matemáticas: Lógica y fundamentos: Lógica computacional: Marcos lógicos