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
[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

Ejemplo extraído de un archivo de teoría

[editar]
subsection{*Definición inductiva de los números pares*}

consts Par :: "nat set"                    | Par de tipo conjunto de naturales
inductive Par                              | Definición inductiva de par
intros
ZeroI: "0 : Par"                           | Cero es par
Add2I: "n : Par ==> Suc(Suc n) : Par"      | n+2 es par si n lo es 

text{* Uso de reglas de introducción: *}
lemma "Suc(Suc(Suc(Suc 0))) \<in> Par"     | 4 es par
apply(rule Add2I)                          | Pasos de la prueba
apply(rule Add2I)
apply(rule ZeroI)
done

text{* Prueba inductiva sencilla: *}
lemma "n:Par ==> n+n : Par"                | 2n es par si n lo es
                                           | Pasos de la prueba
apply(erule Par.induct)                    | Inducción basada en la def. de Par
 apply(simp)                               | simplificación
 apply(rule Par.ZeroI)
apply(simp)
apply(rule Par.Add2I)
apply(rule Par.Add2I)
apply(assumption)
done

Enlaces externos

[editar]