Isabelle
# 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 de la Universidad Técnica de Múnich.

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:

* Sistema de deducción natural
* Inferencia de tipos para verificar que los términos manejados estén bien construidos
* Módulos llamados teorías
* Conjuntos y tipos de datos recursivos
* Inducción estructural
* Facilidades para realizar demostraciones interactivas
* Simplificación por reescritura de términos
