Una herramienta interactiva de prueba de teoremas ( solucionador interactivo de teoremas ) es un software que ayuda al investigador a desarrollar pruebas formales . La evidencia se produce en el proceso de interacción hombre-máquina. Por lo general, dicho software incluye algún tipo de editor de evidencia interactivo u otra interfaz a través de la cual una persona puede buscar evidencia almacenada en la computadora, así como procedimientos automatizados de verificación de evidencia realizados por la computadora.
| Nombre | ultima versión | Desarrolladores | Idioma de implementación | Capacidades | |||||
|---|---|---|---|---|---|---|---|---|---|
| lógica de orden superior | tipos dependientes | núcleo pequeño | Automatización de pruebas | Prueba por reflexión | codigo de GENERACION | ||||
| ACL2 | 8.2 | Matt Kaufmann y J Strother Moore | ceceo común | No | sin tipo | No | Sí | sí [1] | genera código ejecutable |
| Agda | 2.6.0.1 | Ulf Norell, Nils Anders Danielsson y Andreas Abel ( Universidad Tecnológica de Chalmers y Universidad de Gotemburgo ) | Haskell | Sí | Sí | Sí | No | Parcialmente | genera código 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* | en el repositorio | Investigación de Microsoft e INRIA | F* | Sí | Sí | No | Sí | sí [2] | Sí |
| Luz HOL | en el repositorio | Juan Harrison | OCaml | Sí | No | Sí | Sí | No | No |
| HOL4 | Kananaskis-12 (o en el repositorio) | Michael Norrish, Konrad Slind y otros | ML estándar | Sí | No | Sí | Sí | No | Sí |
| Isabelle | 2019 | Larry Paulson ( Cambridge ), Tobias Nipkow ( München ) y Makarius Wenzel | StandardML , 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 Bialystok | pascual libre | Parcialmente | Sí | No | No | No | No |
| NuPRL | 5 | Universidad de Cornell | ceceo común | Sí | Sí | Sí | Sí | desconocido | Sí |
| PVS | 6.0 | ISR Internacional | ceceo común | Sí | Sí | No | Sí | No | desconocido |
| Doce | 1.7.1 | Frank Pfenning y Carsten Schürmann | ML estándar | Sí | Sí | desconocido | No | No | desconocido |
Una interfaz popular para las herramientas interactivas de demostración de teoremas es Proof General, basada en Emacs, desarrollada en la Universidad de Edimburgo . Coq incluye CoqIDE que está escrito en OCaml/ Gtk . Isabelle incluye Isabelle/jEdit, que se basa en jEdit y el marco Isabelle/ Scala para el procesamiento de pruebas centrado en documentos. Para Visual Studio Code , también hay una extensión diseñada para trabajar con Isabelle. Fue desarrollado por Makarius Wenzel [5] .