Demostrador de teoremas Isabelle
Keywords: Demostrador de teoremas Isabelle, ML, Universidad de Cambridge, Technische Universität München, Tobias Nipkow, Larry Paulson, Demostrador de teoremas
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 donde se realizan las pruebas en 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 mas resaltantes de Isabelle se pueden mencionar
- Sistema de deducción natural
- Inferencia de tipos para verificar que los término manejados esten 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 extraido de un archivo de teoría
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 en base a 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