Isabelle

El demostrador interactivo de teoremas "Isabelle" es una herramienta de ayuda a la demostración de teoremas escrita en el lenguaje de programación ML y desarrollada por Larry Paulson de la Universidad de Cambridge y Tobias Nipkow del Technische Universität München.
El lenguaje en el cual se realizan las pruebas es HOL (acrónimo de Higher-Order Logic), que es un lenguaje fuertemente tipificado con estructuras de datos....