Asistente de pruebas

Este artículo incluye una lista de referencias generales , pero permanece en gran parte sin verificar porque carece de suficientes citas en línea correspondientes . Ayude a mejorar este artículo introduciendo citas más precisas. ( Noviembre de 2018 ) ( Obtenga información sobre cómo y cuándo eliminar este mensaje de plantilla )

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 ciencias de la computación 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 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 los proporciona .

Comparación de sistemas

Nombre	Ultima versión	Desarrollador (es)	Lenguaje de implementación	Características
Nombre	Ultima versión	Desarrollador (es)	Lenguaje de implementación	Lógica de orden superior	Tipos dependientes	Grano pequeño	Automatización de pruebas	Prueba por reflejo	Codigo de GENERACION
ACL2	8.3	Matt Kaufmann y J Strother Moore	Lisp común	No	Sin tipo	No	sí	Sí ^[1]	Ya ejecutable
Agda	2.6.2	Ulf Norell, Nils Anders Danielsson y Andreas Abel ( Chalmers y Gotemburgo )	Haskell	sí	sí	sí	No	Parcial	Ya ejecutable
Albatros	0.4	Helmut Brandl	OCaml	sí	No	sí	sí	Desconocido	Aun no implementado
Coq	8.13.2	INRIA	OCaml	sí	sí	sí	sí	sí	sí
F*	repositorio	Microsoft Research e INRIA	F*	sí	sí	No	sí	Sí ^[2]	sí
Luz HOL	repositorio	John Harrison	OCaml	sí	No	sí	sí	No	No
HOL4	Kananaskis-13 (o repositorio)	Michael Norrish, Konrad Slind y otros	ML estándar	sí	No	sí	sí	No	sí
Idris	2 0.4.0.	Edwin Brady	Idris	sí	sí	sí	Desconocido	Parcial	sí
Isabelle	Isabelle2021 (febrero de 2021)	Larry Paulson ( Cambridge ), Tobias Nipkow ( München ) y Makarius Wenzel	ML estándar , Scala	sí	No	sí	sí	sí	sí
Inclinarse	v3.4.2 ^[3]	Investigación de Microsoft	C ++	sí	sí	sí	sí	sí	Desconocido
LEGO (no afiliado a Lego )	1.3.1	Randy Pollack ( Edimburgo )	ML estándar	sí	sí	sí	No	No	No
Mizar	8.1.05	Universidad de Białystok	Pascal libre	Parcial	sí	No	No	No	No
NuPRL	5	Universidad de Cornell	Lisp común	sí	sí	sí	sí	Desconocido	sí
PVS	6.0	SRI Internacional	Lisp común	sí	sí	No	sí	No	Desconocido
Duodécimo	1.7.1	Frank Pfenning y Carsten Schürmann	ML estándar	sí	sí	Desconocido	No	No	Desconocido

ACL2 : un lenguaje de programación, una teoría lógica de primer orden y un demostrador de teoremas (con modos tanto interactivos como automáticos) en la tradición de Boyer-Moore.
Coq : que 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 del teorema HOL : una familia de herramientas derivada 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 solo pueden introducirse a través de "estrategias" que garantizan la corrección lógica. La composición de la estrategia brinda a los usuarios la capacidad de producir pruebas significativas con relativamente pocas interacciones con el sistema. Los miembros de la familia incluyen:
- HOL4 - El "descendiente principal", todavía en desarrollo activo. Soporte para Moscow ML y Poly / ML . Tiene una licencia estilo BSD .
- HOL Light : una próspera "horquilla 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 ^[4]

Isabelle es una demostradora de teoremas interactiva, sucesora de HOL. El código base principal tiene licencia BSD, pero la distribución de Isabelle incluye muchas herramientas complementarias con diferentes licencias.
Jape : basado en Java.
Inclinarse
LEGO
Matita : un sistema de luz basado en el cálculo de construcciones inductivas.
MINLOG : un asistente de pruebas basado en una 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 una lógica de orden superior que es extensible.
Sistema de verificación de prototipos (PVS): un lenguaje de prueba y un sistema basado en lógica de orden superior.
TPS y ETPS : demostradores de teoremas interactivos también basados en el cálculo lambda de tipo simple, pero basados en una formulación independiente de la teoría lógica y la implementación independiente.
Typelab
Milenrama

El Museo de Probadores de Teoremas es una iniciativa para conservar las fuentes de los sistemas de probadores de teoremas para análisis futuros, ya que son importantes artefactos culturales / científicos. Tiene las fuentes de muchos de los sistemas mencionados anteriormente.

Interfaces de usuario

Un front-end popular para asistentes de pruebas es el 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, Makarius Wenzel también ha desarrollado una extensión de Visual Studio Code para Isabelle. ^[5]

Ver también

Demostración automatizada de teoremas
Prueba asistida por computadora
Manifiesto QED
Verificación formal
Teorías del módulo de satisfacción
Metamath : un lenguaje para desarrollar matemáticas formalizadas acompañado de un corrector de pruebas para este lenguaje y varias bases de datos de miles de teoremas probados.

Notas

^ Caza, Warren; Matt Kaufmann; Robert Bellarmine Krug; J Moore; Eric W. Smith (2005). "Meta razonamiento en ACL2" (PDF) . Demostración de teoremas en lógicas de orden superior . Apuntes de conferencias en Ciencias de la Computación. 3603 . págs. 163-178. doi : 10.1007 / 11541868_11 . ISBN 978-3-540-28372-0.
^ Busque "pruebas por reflexión": arXiv : 1803.06547
^ "Página de versiones de Lean Theorem Prover" . GitHub .
^ Granjero, William M .; Guttman, Joshua D .; Thayer, F. Javier (1993). "IMPS: un sistema interactivo de prueba matemática" . Revista de razonamiento automatizado . 11 (2): 213–248. doi : 10.1007 / BF00881906 . S2CID 3084322 . Consultado el 22 de enero de 2020 .
↑ Wenzel, Makarius. "Isabelle" . Consultado el 2 de noviembre de 2019 .

Referencias

Henk Barendregt y Herman Geuvers (2001). "Ayudantes de pruebas que utilizan sistemas de tipo dependiente" . En Manual de razonamiento automatizado .
Frank Pfenning (2001). "Marcos lógicos" . En Manual de razonamiento automatizado .
Frank Pfenning (1996). "La práctica de los marcos lógicos".
Robert L. Constable (1998). "Tipos en informática, filosofía y lógica". En el Manual de teoría de la prueba .
H. Geuvers. " Asistentes de prueba: Historia, ideas y futuro ".
Freek Wiedijk. " Los diecisiete probadores del mundo "

enlaces externos

"Introducción" a la programación certificada con tipos dependientes .
Introducción al Coq Proof Assistant (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
Grupos y sistemas de deducción automatizados
Demostración de teoremas y sistemas de razonamiento automatizado
Base de datos de sistemas de razonamiento mecanizado existentes
NuPRL: otros sistemas
Implementaciones y marcos lógicos específicos
DMOZ : Ciencias: Matemáticas: Lógica y fundamentos: Lógica computacional: Marcos lógicos

[1] Caza, Warren; Matt Kaufmann; Robert Bellarmine Krug; J Moore; Eric W. Smith (2005). "Meta razonamiento en ACL2" (PDF) . Demostración de teoremas en lógicas de orden superior . Apuntes de conferencias en Ciencias de la Computación. 3603 . págs. 163-178. doi : 10.1007 / 11541868_11 . ISBN 978-3-540-28372-0.

[2] Busque "pruebas por reflexión": arXiv : 1803.06547

[3] "Página de versiones de Lean Theorem Prover" . GitHub .

[4] Granjero, William M .; Guttman, Joshua D .; Thayer, F. Javier (1993). "IMPS: un sistema interactivo de prueba matemática" . Revista de razonamiento automatizado . 11 (2): 213–248. doi : 10.1007 / BF00881906 . S2CID 3084322 . Consultado el 22 de enero de 2020 .

[5] Wenzel, Makarius. "Isabelle" . Consultado el 2 de noviembre de 2019 .

[1]