Hispanopedia Wiki
Articulo de referencia

Asistente de pruebas

Una sesión de demostración interactiva en RocqIDE, que muestra el script de demostración a la izquierda y el estado de la demostración a la derecha. En informática y lógica mate...

Hispanopedia WikiContenido en espanolLectura gratuita
Una sesión de demostración interactiva en RocqIDE, que muestra el script de demostración a la izquierda y el estado de la demostración a la derecha.

En informática y lógica matemática , un asistente de demostración o demostrador interactivo de teoremas es una herramienta de software que facilita el desarrollo de demostraciones 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 demostraciones, cuyos detalles se almacenan en un ordenador , que también proporciona algunos pasos .

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 ]

Verificación de pruebas automatizada

La verificación automatizada de pruebas consiste en utilizar software para comprobar la corrección de las demostraciones . Es uno de los campos más desarrollados del razonamiento automatizado . Se diferencia de la demostración automatizada de teoremas en que la verificación automatizada simplemente comprueba mecánicamente el funcionamiento formal de una demostración existente, en lugar de intentar desarrollar nuevas demostraciones o teoremas. Por ello, la tarea de verificación automatizada de pruebas es mucho más sencilla que la de la demostración automatizada de teoremas, lo que permite que el software de verificación automatizada de pruebas sea mucho más simple que el software de demostración automatizada de teoremas.

Debido a su reducido tamaño, algunos sistemas automatizados de verificación de pruebas pueden tener menos de mil líneas de código fuente, lo que permite tanto la verificación manual como la verificación automatizada por software. Los sistemas Mizar , HOL Light y Metamath son ejemplos de sistemas automatizados de verificación de pruebas. La verificación automatizada de pruebas puede realizarse mediante un proceso por lotes o de forma interactiva, como parte de un sistema interactivo de demostración de teoremas .

Historia

Automath , desarrollado por Nicolaas Govert de Bruijn a partir de 1967, suele considerarse el primer verificador de pruebas y el primer sistema en utilizar la correspondencia de Curry-Howard entre programas y pruebas. [ 2 ] Automath fue utilizado por L.S. van Benthem Jutting en 1977 para formalizar los Fundamentos del Análisis de Landau , que constituyeron la primera formalización de los números reales. [ 3 ]

En 1973, Robert Boyer y J Moore publicaron Proving Theorems about LISP Functions , cuyo objetivo era verificar programas, no matemáticas. [ 4 ] Su demostrador de teoremas ahora se conoce como ACL2 .

En la década de 1970, Edinburgh LCF introdujo la idea de utilizar un lenguaje de programación funcional como metalenguaje para un demostrador de teoremas, lo que dio lugar a la familia HOL de asistentes de demostración. [ 3 ]

En la década de 1990 surgió Rocq (entonces conocido como Coq), que se ha utilizado en numerosos proyectos de formalización a gran escala . Desde finales de la década de 2010, Lean , un asistente de demostración fuertemente influenciado por Rocq, se ha convertido en otra opción popular, especialmente para formalizar las matemáticas.

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.
  • Demostradores de teoremas HOL : una familia de herramientas derivadas 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 nuevos elementos del lenguaje y solo pueden introducirse mediante "estrategias" que garantizan la corrección lógica. La composición de estrategias permite a los usuarios generar demostraciones significativas con relativamente pocas interacciones con el sistema. Algunos miembros de la familia son:
  • IMPS, un sistema interactivo de demostración matemática. [ 11 ]
  • Isabelle es un demostrador de teoremas interactivo que permite la codificación de otros sistemas. Isabelle/HOL es su instancia más popular, cuya base es similar a la del demostrador HOL. Otras instancias incluyen Isabelle/ZF e Isabelle/FOL [ 12 ] . El código base principal tiene licencia BSD, pero la distribución de Isabelle incluye numerosas herramientas complementarias con diferentes licencias.
  • Japón – Basado en Java.
  • Lean es un demostrador de teoremas interactivo y un lenguaje de programación funcional con tipado dependiente. Se basa en el cálculo de construcciones inductivas con universos no acumulativos. Desde la versión 4 (lanzada en 2023), es autoalojado. Puede utilizarse para formalizar las matemáticas (y cuenta con una amplia y coherente biblioteca para matemáticas formales), así como para la verificación de software y hardware.
  • LEGO
  • Matita – Un sistema ligero basado en el cálculo de construcciones inductivas.
  • MINLOG : un asistente de demostración basado en lógica mínima de primer orden.
  • Mizar : un asistente de demostración basado en lógica de primer orden, con un estilo de deducción natural , y en la teoría de conjuntos de Tarski-Grothendieck .
  • PhoX : un asistente de demostración basado en lógica de orden superior que es extensible.
  • Sistema de Verificación de Prototipos (PVS): un lenguaje y sistema de demostración basado en lógica de orden superior.
  • Rocq (anteriormente llamado Coq ): un popular demostrador de teoremas interactivo basado en el cálculo de construcciones inductivas.
  • Sistema de Demostración de Teoremas (TPS) y ETPS: demostradores de teoremas interactivos también basados ​​en cálculo lambda tipado simple, pero basados ​​en una formulación independiente de la teoría lógica y una implementación independiente.

Interfaces de usuario

Un front-end comúnmente utilizado para asistentes de demostración era Proof General, basado en Emacs y desarrollado en la Universidad de Edimburgo . Hoy en día, muchos demostradores incluyen su propio editor. Rocq incluye RocqIDE, basado en OCaml/ Gtk . Isabelle incluye Isabelle/jEdit, basado 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 Rocq, [ 13 ] Isabelle por Makarius Wenzel, [ 14 ] y para Lean 4 por los desarrolladores de leanprover. [ 15 ]

Alcance de la formalización

Freek Wiedijk ha estado elaborando una clasificación de asistentes de demostración según la cantidad de teoremas formalizados de una lista de 100 teoremas conocidos. A septiembre de 2025, solo seis sistemas habían formalizado demostraciones de más del 70 % de los teoremas: Isabelle, HOL Light, Lean, Rocq, Metamath y Mizar. [ 16 ] [ 17 ]

Pruebas formalizadas destacadas

A continuación se presenta una lista de demostraciones destacadas que se han formalizado en asistentes de demostración.

Véase también

Referencias

  1. ↑ Ornes, Stephen (27 de agosto de 2020). "Quanta Magazine: ¿Qué tan cerca están las computadoras de automatizar el razonamiento matemático?" .
  2. ↑ Geuvers, Herman (16 de julio de 2009). "Asistentes de prueba: historia, ideas y futuro" (PDF) . Sādhanā . 34 : 3–25 .
  3. 1 2 Paulson, Lawrence (23 de abril de 2026). "¿Por qué no usar Lean?" . Recuperado el 23 de abril de 2026 .
  4. ↑ Boyer, Robert; Moore, J. "Demostración de teoremas sobre funciones LISP" . Association for Computing Machinery . 22 : 129–144 .
  5. ↑ Hunt, Warren; Kaufmann, Matt ; Krug, Robert Bellarmine; Moore, J.; Smith, Eric W. (2005). "Meta Reasoning in ACL2" (PDF) . Theorem Proving in Higher Order Logics . Lecture Notes in Computer Science. Vol. 3603. pp. 163–178 . doi : 10.1007/11541868_11 . ISBN   978-3-540-28372-0.
  6. 1 2 3 "agda/agda: Agda es un lenguaje de programación con tipado dependiente / demostrador de teoremas interactivo" . GitHub . Consultado el 31 de julio de 2024 .
  7. ↑ «La Wiki de Agda» . Consultado el 31 de julio de 2024 .
  8. ↑ Buscar "demostraciones por reflexión": arXiv : 1803.06547
  9. ↑ "Página de lanzamientos de Lean 4" . GitHub . Consultado el 22 de septiembre de 2025 .
  10. ↑ "Versión v0.198 metamath/Metamath-exe" . GitHub .
  11. ↑ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier (1993). "IMPS: Un sistema interactivo de demostración matemática" . Journal of Automated Reasoning . 11 (2): 213– 248. doi : 10.1007/BF00881906 . S2CID 3084322. Consultado el 22 de enero de 2020 . 
  12. ↑ Página web de documentación de Isabelle. Consultada el 22 de abril de 2026: https://isabelle.in.tum.de/documentation.html
  13. ↑ "coq-community/vscoq" . 29 de julio de 2024 – vía GitHub.
  14. ↑ Wenzel, Makarius. "Isabelle" . Consultado el 2 de noviembre de 2019 .
  15. ↑ "VS Code Lean 4" . GitHub . Consultado el 15 de octubre de 2023 .
  16. ^ Wiedijk, Freek (22 de septiembre de 2025). "Formalizando 100 teoremas" .
  17. ↑ 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 . 
  18. ↑ 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) del original el 5 de agosto de 2011 
  19. ↑ "Feit thomson demostrado en coq - Centro Conjunto Inria de Investigación de Microsoft" . 19 de noviembre de 2016. Archivado del original el 19 de noviembre de 2016. Consultado el 7 de diciembre de 2023 .
  20. ↑ Licata, Daniel R.; Shulman, Michael (2013). "Cálculo del grupo fundamental del círculo en la teoría de tipos homotópicos". 28.º Simposio Anual ACM/IEEE de Lógica en Ciencias de la Computación de 2013. pp. 223–232 . arXiv : 1301.3443 . doi : 10.1109/lics.2013.28 . ISBN  978-1-4799-0413-6. S2CID 5661377 . 
  21. ↑ "Problema matemático que tardó 3500 años en resolverse finalmente encuentra solución" . IFLScience . 11 de marzo de 2022. Consultado el 9 de febrero de 2024 .
  22. ↑ Avigad, Jeremy (2023). "Matemáticas y el giro formal". arXiv : 2311.00007 [ math.HO ].
  23. ^ Sloman, Leila (6 de diciembre de 2023). "El "equipo A" de las matemáticas demuestra un vínculo crucial entre la suma y los conjuntos . Quanta Magazine . Consultado el 7 de diciembre de 2023 .
  24. ↑ "Hemos demostrado que "BB(5) = 47.176.870"" . El desafío del castor ocupado . 2024-07-02 . Consultado el 2024-07-09 .

Referencias

  • Barendregt, Henk ; Geuvers, Herman (2001). "18. Asistentes de demostración que utilizan sistemas de tipos dependientes" (PDF) . En Robinson, Alan JA; Voronkov, Andrei (eds.). Manual de razonamiento automatizado . Vol.  2. Elsevier. pp.  1149–. ISBN 978-0-444-50812-6Archivado del original (PDF) el 27 de julio de 2007.
  • Pfenning, Frank . "17. Marcos lógicos" (PDF) . Manual vol. 2 2001. pp. 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 . Lecture Notes in Computer Science. Vol.  1059. Springer. pp. 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 demostración . Estudios de lógica. Vol.  137. Elsevier. pp. 683–786 . ISBN  978-0-08-053318-6.
  • Wiedijk, Freek (2005). "Los diecisiete probadores del mundo" (PDF) . Universidad Radboud de Nimega.
  • Museo de Demostradores de Teoremas
  • "Introducción" en 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 la demostración de teoremas
Catálogos
  • Matemáticas digitales por categoría: Demostradores tácticos
  • Sistemas y grupos de deducción automatizada
  • Sistemas de demostración de teoremas y razonamiento automatizado
  • Base de datos de sistemas de razonamiento mecanizado existentes
  • NuPRL: Otros sistemas
  • "Marcos lógicos específicos e implementaciones" . Archivado del original el 10 de abril de 2022. Consultado el 15 de febrero de 2024 .(Por Frank Pfenning).
  • DMOZ : Ciencia: Matemáticas: Lógica y Fundamentos: Lógica Computacional: Marcos Lógicos