title: Isabelle
text: # 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
  