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 | |||||
---|---|---|---|---|---|---|---|---|---|
Lógica de orden superior | Tipos dependientes | Grano pequeño | Automatización de pruebas | Prueba por reflejo | Codigo de GENERACION | ||||
ACL2 | 8.2 | Matt Kaufmann y J Strother Moore | Lisp común | No | Sin tipo | No | sí | Sí [1] | Ya ejecutable |
Agda | 2.6.0.1 | 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.11.0 | 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.3.0. | Edwin Brady | Idris | sí | sí | sí | Desconocido | Parcial | sí |
Isabelle | Isabelle2020 (abril de 2020) | 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 la empresa 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