asistente de prueba
En ciencias de la computación y lógica matemática , un asistente de prueba o probador de teoremas interactivo es una herramienta de software para ayudar con el desarrollo de pruebas formales mediante la colaboración hombre-máquina. Esto implica algún tipo de editor de prueba interactivo u otra interfaz , con la que un ser humano puede guiar la búsqueda de pruebas, cuyos detalles se almacenan y algunos pasos proporcionados por una computadora .
Theorem Prover Museum es una iniciativa para conservar las fuentes de los sistemas de demostración de teoremas para futuros análisis, ya que son importantes artefactos culturales/científicos. Tiene las fuentes de muchos de los sistemas mencionados anteriormente.
Un front-end popular para asistentes de prueba es 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 de Isabelle/ Scala para el procesamiento de pruebas orientado a documentos. Más recientemente, Makarius Wenzel también desarrolló una extensión de Visual Studio Code para Isabelle. [5]
