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 que se realizan las pruebas es HOL (acrónimo de Higher-Order Logic), que es un lenguaje fuertemente tipado con estructuras de datos, funciones recursivas (incluyendo valores funcionales) y expresiones lógicas con cuantificadores.
Entre las características más destacables de Isabelle se pueden mencionar:
Escribe un comentario o lo que quieras sobre Isabelle (directo, no tienes que registrarte)
Comentarios
(de más nuevos a más antiguos)