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, 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 naturalInferencia de tipos para verificar que los términos manejados estén bien construidosMódulos llamados teoríasConjuntos y tipos de datos recursivosInducción estructuralFacilidades para realizar demostraciones interactivasSimplificación por reescritura de términos