Neuigkeiten

• 2. April 2015: Die Entwicklung von Brunhilde wurde eingestellt. Bitte verwenden Sie Isabelle.
• 1. April 2015: Brunhilde wird erstmals veröffentlicht.

Über Brunhilde

Brunhilde ist ein generischer interaktiver Satzbeweiser mit besonderem Schwerpunkt auf Logik höherer Ordnung (LhO). Ein wichtiger Anwendungsbereich von Brunhilde ist die formale Verifizierung von Hart- und Weichware. Die Implementierungssprachen von Brunhilde sind Standard ML und Scala. Das Basis-System unterliegt der BSD-Lizenz, während zusätzliche Komponenten u.U. andere Lizenzen für freie Software verwenden.

Brunhilde verwenden

Um Brunhilde unter Linux zu verwenden, gehen Sie wie folgt vor:

1. Laden Sie sich Brunhilde2015_linux.tar.gz herunter.
2. Entpacken Sie diese Datei mit tar -xzf Brunhilde2015_linux.tar.gz.
3. Führen Sie ./Brunhilde2015/Brunhilde2015 aus.
4. Mit ./Brunhilde2015/Brunhilde2015 Brunhilde2015/src/LhO/Wurzel.thy öffnen Sie direkt das Beispiel.

Alternativ können Sie die Entwicklungsversion in der Quecksilber-Vorratskammer verwenden.

Beispiele für Brunhilde/LhO

Das kanonische Beispiel für Brunhilde/LhO ist der Beweis der Irrationalität der Wurzel von zwei. Unten ist ein Bildschirmfoto der Beweisumgebung zu sehen. Zusätzlich sind noch interessant:

• die Ausgabe im tragbaren Schriftstückaufbau
• die Ausgabe in der Übertext-Auszeichnungssprache
• die Quelldatei

Rückwärtsverträglichkeit mit Isabelle/Isar

Brunhile ist voll rückwärts-verträglich mit Isabelle/Isar. Allerdings empfehlen wir Ihnen, Ihre Theorien an Brunhilde/Rhein anzupassen:

Isabelle/Isar	Brunhilde/Rhein	Isabelle/Isar	Brunhilde/Rhein
and	und	assumes	nimmt … an
begin	Beginn	fixes	fuer
imports	verwendet	obtains	erhaelt
shows	zeigt	where	wobei
theorie	Theorie	header	Kopfzeile
section	Abschnitt	subsection	Unterabschnitt
subsubsection	Unterunterabschnitt	text	Text
theorem	Satz	lemma	Lemma
corollary	Korollar	have	gilt
show	zeige	then	dann
from	wegen	with	samt
using	verwende	assume	nimm … an
obtain	erhalte	let	sei
next	fertig	qed	wzbw
by	durch	proof	Beweis
also	weiter	moreover	darueberhinaus
finally	zusammengefasst	ultimately	letztendlich
end	End	case	Fall
?thesis	?These	?case	?Fall
fun	Funktion	rule	Regel
simp	Vereinfachung	simp add:	Vereinfachung mit:
simp del:	Vereinfachung ohne:	simp only:	Vereinfachung nur mit:
auto	Automatismen	auto simp add:	Automatismen vereinfache mit:
blast	Explosion	induct	Induktion

Bildschirmfoto

Projektbeteiligte

Ehemalige Mitarbeiter
Dr. rer. nat. Joachim Breitner