Isabelle

De Wikipedia, la enciclopedia libre
Saltar a: navegación, búsqueda
Isabelle
Autor
Lawrence Paulson
http://isabelle.in.tum.de/
Información general
Última versión estable Isabelle2012
Género Software matemático
Programado en Standard ML
Sistema operativo Linux, Mac OS X y Windows
Licencia Licencia BSD

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