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
Ejemplo extraído 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 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
- Página de Isabelle
Datos: Q460340