Isabelle

Isabelle
Información general
Tipo de programa	Software matemático
Autor	Lawrence Paulson
Lanzamiento inicial	1986
Licencia	Licencia BSD
Información técnica
Programado en	Standard ML
Versiones
Última versión estable	Isabelle2015 ()
Archivos legibles
Isabelle file format
Archivos editables
Isabelle file format
Enlaces
Sitio web oficial
[editar datos en Wikidata]

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