IsaMorph

IsaMorph ist eine Linux-Distribution Live CD (basierend auf Morphix) mit den interaktiven Theorembeweiser Isabelle.
Das bedeutet, Sie von der CD booten und erhalten Sie einen voll funktionsfähigen "Beweisen" Umwelt, ohne die Installation GNU / Linux oder Isabelle kann. Legen Sie einfach die CD in Ihren PC und haben fünf Minuten später den ersten Satz bewiesen.
Alle Programme, die innerhalb IsaMorph verteilt sind freie Software. Dies bedeutet, dass das Betriebssystem und die in dieser CD-Anwendungen können frei kopiert, modifiziert und verteilt werden. Also zögern Sie nicht, Kopien an Ihre Freunde oder Kollegen zu geben.
Legen Sie die CD in das CD-Laufwerk auf einem Intel-kompatibler PC oder Laptop. Nun starten Sie den Computer. Stellen Sie sicher, dass das erste Boot-Gerät ist CD. Dazu müssen Sie die BIOS-Einstellungen des Computers ändern.
Wenn Sie nicht damit vertraut sind, erhalten Sie Hilfe von Ihrem Systemadministrator oder jemand, der weiß, wie es geht. Während der Computer gestartet booten, wird es für eine CD in das Laufwerk zu suchen. Ein Menü wird nach einiger Zeit angezeigt.
Drücken Sie einfach die Enter-Taste oder warten Sie für einige Zeit. Der Computer wird weiterhin von der CD booten und hoffentlich geben Ihnen einen grafischen Bildschirm ähnlich dem, was Sie kennen. Sie können auf das Menü oben links klicken und starten Sie Anwendungen.
IsaMorph enthält eine voll funktionsfähige Isabelle Umgebung unterstützen Arzneimittelprüfung und Erstellung von Dokumenten umfasst dies:
Isabelle (Version 2005)
Mit dem interaktiven Theorembeweiser Isabelle 2005 und mit zumindest den folgenden Logiken in zusammengestellt: HOL, HOL-Complex, ZF, FOL, und Pure. So nach dem Booten IsaMorph können Sie sofort beweisen Theoreme in jeder dieser Logiken. Die CD enthält eine Offline-Version von Isabelle Tutorials und Theorie Dokumentation.
HOL-TestGen (Version 1.1.1)
Ein Testfall-Generator für Spezifikation Unit-Tests. Es ist auf der Oberseite des specfication und Theorembeweiser Isabelle / HOL gebaut.
Proof General (Version 3.6pre)
Eine leistungsstarke Benutzeroberfläche für Isabelle.
SML von New Jersey (Version 110.56)
Der Standard ML Environment verwendet für die Erstellung und Ausführung von Isabelle.
GNU Emacs (Version 22.0.50)
Der GNU Emacs Editor, der mit Proof General der Hauptbenutzerschnittstelle von Isabelle zusammen baut.
teTeX (Version 2.0.2)
Ein komplettes LaTeX-Umgebung für die Generierung von Beweisdokumenten verwendet.
Andere Anwendungen
Darüber hinaus enthält die CD auch eine Vielzahl von Anwendungen für eine gemeinsame Nutzung. Es beinhaltet eine benutzerfreundliche Desktop (Gnome) einen Internet-Browser (Mozilla), und so weiter. Werfen Sie einen Blick auf die Speisekarte, um herauszufinden, viele mehr. Ich habe versucht, die Anzahl der nicht Isabelle spezifische Software zu minimieren, um die Download-Größe minimieren.
Was ist neu in dieser Version: