Isabelle

Archiu:Isabelle jedit.png

Isabelle

El demostrador interactiu de teoremes Isabelle és una ferramenta d'ajuda a la demostració de teoremes escrita en el llenguage de programació ML i desenrollada per Larry Paulson de l'Universitat de Cambridge i Tobias Nipkow de l'Universitat Tècnica de Munich.

El llenguage en que es realisen les proves és HOL (acrònim de Higher-Order Logic), que és un llenguage fortament tipado en estructures de senyes, funcions recursivas (incloent valors funcionals) i expressions llògiques en quantificadors.

Entre les característiques més destacables d'Isabelle es poden mencionar:

Sistema de deducció natural Inferència de tipos per a verificar que els térmens manejats estiguen ben construïts Mòduls cridats teories Conjunts i tipos de senyes recursivos Inducció estructural Facilitats per a realisar demostracions interactives Simplificació per reescritura de térmens

Eixemple extret d'un archiu de teoria

subsection{Definició inductiva dels número par*}

consts Parell :: "nat set"                    | Parell de tipo conjunt de naturals
inductive Parell                              | Definició inductiva de parell
intros
ZeroI: "0 : Parell"                           | Zero és parell
Add2I: "n : Parell ==> Suc(Suc n) : Parell"      | n+2 és parell si n ho és 

text{* Us de regles d'introducció: *}
lemma "Suc(Suc(Suc(Suc 0))) <in> Parell"     | 4 és parell
apply(rule Add2I)                          | Passos de la prova
apply(rule Add2I)
apply(rule ZeroI)
done

text{* Prova inductiva senzilla: *}
lemma "n:Parell ==> n+n : Parell"                | 2n és parell si n ho és
                                           | Passos de la prova
apply(erule Parell.induct)                    | Inducció basada en la def. de Parell
 apply(simp)                               | simplificació
 apply(rule Parell.ZeroI)
apply(simp)
apply(rule Parell.Add2I)
apply(rule Parell.Add2I)
apply(assumption)
done