IsaMorph: Ein sofort lauffähiges Isabelle Setup

IsaMorph ist eine GNU/Linux Live CD (basierend auf Morphix) für den interaktiven Theorembeweiser Isabelle, d.h. ohne eine Installation von GNU/Linux oder Isabelle kann direkt von der CD gestartet werden. Einfach die CD in den Rechner legen und fünf Minuten später sind bereits die ersten Theoreme bewiesen.

Alle Programme auf der IsaMorph CD sind Freie Software, d.h. das Betriebsystem und alle Anwendungen auf der CD können frei kopiert, abgeändert und weitergegeben werden.

Wie wird die CD gestartet?

Einfach die CD in das CD-Laufwerk eines Intel kompatiblen PCs oder Laptop legen und den Computer neu starten. Stellen Sie sicher, dass das der Rechner auch von CD startet (bootet). Eventuell müssen Sie hierzu die BIOS Einstellungen ändern. Wenn der Rechner startet sollte er nach einer CD suchen und nach einer kurzen Zeit ein Menü auf dem Bildschirm anzeigen. Nach kurzer Pause wird der Rechner weiter von CD starten und (hoffentlich) eine graphische Benutzeroberfäche anzeigen. Sie können links oben auf das Menü klicken, um Anwendungen zu starten.

IsaMorph 0.2.1 screenshot

Was ist auf der CD?

IsaMorph enthält eine sofort arbeitsfähige Isabelle Umgebung die auch die Generierung von Beweisdokumenten unterstützt. Die CD umfasst:

Isabelle (Version 2005)
Der interaktive Theorem-Beweiser Isabelle 2005. Auf der CD sind mindestens die folgenden Logiken ("fix-und-fertig") vorinstalliert: HOL, HOL-Complex, ZF, FOL, and Pure. Nach dem starten von IsaMorph können sofort Theoreme in jeder dieser Logiken bewiesen werden. Die CD enthält zudem die Isabelle Tutorials und Theorie-Dokumentationen.
HOL-TestGen (Version 1.1.1)
Ein Test-Daten Generator für den spezifikationsbasierten Unit-Test. HOL-TestGen ist eine Erweiterung des interaktiven Theorembeweisers Isabelle/HOL.
Proof General (Version 3.6pre)
Eine mächtige Benutzeroberfläche für Isabelle.
SML of New Jersey (Version 110.56)
Die Standard ML Umgebung die für die Ausführung von Isabelle verwendet wird.
GNU Emacs (Version 22.0.50)
Der GNU Emacs Texteditor, der zusammen mit Proof General die Benutzerschnittstelle von Isabelle zur Verfügung stellt.
teTeX (Version 2.0.2)
Eine vollständige LaTeX Umgebung, die Isabelle zur Generierung von Beweisdokumenten verwendet.
Weitere Anwendungen
Zusätzlich enthält die CD eine Vielzahl "gewöhnlichen" Anwendungen, dies umfasst z.B. einen benutzerfreundlichen Desktop (Gnome) oder einen Internet Browser (Mozilla). Schauen Sie sich einfach die Menüs an, um herauszufinden was es sonst noch gibt. Ich habe versucht, möglichst wenige "nicht Isabelle-spezifische" Anwendungen auf die CD zu installieren, um die Grösse des Downloads zu minimieren.

Download Version 0.9

IsaMorph-0.9.iso (ca. 498 MByte, MD5: e84b47a3e736fb4bf70776b789a40623) changelog