asistente de pruebas

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. ^[6]
• 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 de iluminación 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 prueba basado en la lógica de primer orden, en un estilo de deducción natural , y la teoría de conjuntos de Tarski-Grothendieck .
• PhoX  : un asistente de pruebas basado en lógica de orden superior que es 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 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, Makarius Wenzel ^[7] desarrolló extensiones de Visual Studio Code para Isabelle y los desarrolladores de leanprover para Lean 4. ^[8]

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. ^{[9] [10]}

Pruebas formalizadas notables

La siguiente es una lista de pruebas notables que se han formalizado en los asistentes de prueba.

Ver también

• Demostración automatizada de teoremas  : subcampo del razonamiento automatizado y la lógica matemática
• Prueba asistida por computadora  : prueba matemática generada al menos parcialmente por computadora
• Verificación formal  : probar o refutar la exactitud de ciertos algoritmos previstos.
• Manifiesto QED  : propuesta para una base de datos informática de todos los conocimientos matemáticos
• Teorías del módulo de satisfacción  : 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). "Revista Quanta: ¿Qué tan cerca están las computadoras de automatizar el razonamiento matemático?".
2. 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. ISBN 978-3-540-28372-0.
3. Busque "pruebas por reflexión": arXiv :1803.06547
4. "Página de lanzamientos de Lean 4". GitHub . Consultado el 15 de octubre de 2023 .
5. "Lanzamiento v0.198 · ​​metamath/Metamath-exe". GitHub .
6. 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 .
7. Wenzel, Makario. "Isabel" . Consultado el 2 de noviembre de 2019 .
8. "Código VS Lean 4". GitHub . Consultado el 15 de octubre de 2023 .
9. Wiedijk, Freek (15 de septiembre de 2023). "Formalizando 100 teoremas".
10. 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.
11. Gonthier, Georges (2008), "Prueba formal: el teorema de los cuatro colores" (PDF) , Avisos de la Sociedad Matemática Estadounidense , 55 (11): 1382–1393, MR  2463991, archivado (PDF) desde el original en 2011 -08-05
12. "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 .
13. 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. ISBN 978-1-4799-0413-6. S2CID  5661377 . Consultado el 7 de diciembre de 2023 .
14. "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 .
15. Avigad, Jeremy. «LAS MATEMÁTICAS Y EL TURNO FORMAL» (PDF) . arXiv .
16. 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 .

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 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 mecanizados 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