Isabelle
Biografía
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