Ludwig-Maximilians-Universität München, Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik

Fortgeschrittenenpraktikum

Visualisierung des Kalküls des Natürlichen Schließens

Inhalt

Der Kalkül des natürlichen Schließens ist einer der wichtigsten elementaren Formalismen der Logik. Trotz seiner engen Anlehnung an die natürliche Denkweise des Menschen ist er Nicht-Logikern nicht ohne weiteres zugänglich, da er das abstrakte Arbeiten mit Formeln und logischen Symbolen erfordert.

Aufgabe dieser Projektarbeit war es, eine Visualisierung des natürlichen Schließens zu entwerfen, die möglichst ohne Formeln auskommen sollte. Dazu sollte ein Java-Programm entwickelt werden, das es auch Benutzern ohne jegliche mathematische und logische Vorbildung erlauben sollte, auf spielerische Art und Weise mit dem Kalkül des natürlichen Schließens zu experimentieren.

Das Ergebnis der Arbeit ist eine vollkommen grafische Notation für das natürliche Schliessen, die sich stark an das allseits bekannte Domino-Spiel anlehnt. Damit das System nicht zu komplex und damit für Benutzer ohne logisches Hintergrundwissen unbenutzbar wird, ist es auf klassische Aussagenlogik beschränkt (eine Erweiterung wäre jedoch möglich).

Das Java-Programm, das die Domino-Notation umsetzt, ermöglicht das Führen eines Beweises durch das Aneinandersetzen von Dominosteinen. Dabei kann jederzeit der equivalente Beweis in Formel-Notation angezeigt werden. Zusätzlich zum eigentlichen Domino-Programm wurden weitere Programm entwickelt, die intern mit den Domino-Datenstrukturen arbeiten: ein interaktiver Beweiser im Textmodus, ein Tautologie-Generator und ein automatischer Beweiser, der den Schwierigkeitsgrad eines Beweises bewertet.

Materialien

• Zusammenfassung (PDF, 79K)
• Quelltexte und ausführbares Java-Programm (JAR, 312K)
• Programm als Applet on-line starten

Bearbeiter: Matthias S. Benkmann
Aufgabensteller: Dr. Stephan Merz
Betreuer: Dr. Stephan Merz
Fertigstellung: September 2002