3.1.2 Umformung

Abbildung 1: Programm nach dem Start

Nach dem Start präsentiert sich das Programm wie in Abbildung 1 zu sehen. In das große Textfeld kann eine beliebige aussagenlogische Formel eingegeben werden. Die elf Schaltflächen unterhalb des Eingabefeldes können verwendet werden, um Funktionssymbole einzugeben, die nicht über die Tastatur eingegeben werden können.

Die Syntax für eine solche Formel orientiert sich an der in Kapitel 2.1 beschriebenen Syntax, mit folgenden Unterschieden:

• Unter Berücksichtigung der Assoziativität von Konjunktion, Disjunktion, Antivalenz und Äquivalenz dürfen Klammern weggelassen werden. So kann zum Beispiel statt $\left(A \vee \left(B \vee C\right)\right)$ auch $\left(A \vee B \vee C\right)$ geschrieben werden; derartige Formeln werden automatisch rechtsassoziativ geklammert, damit das Programm damit arbeiten kann.
• Die Klammern, welche die gesamte Formel umschließen, dürfen weggelassen werden ( $\left(A \wedge B\right)$ wird zu $A \wedge B$). Diese Klammern werden automatisch ergänzt.

Die Grammatik, die vom Parser verwendet wird, wird in Kapitel 3.3 exakt beschrieben.

Als Variablen sind Zeichenketten erlaubt, die

• aus einem einzigen Groß-/Kleinbuchstaben bestehen, wobei t und f nicht erlaubt sind (diese Symbole sind für die Konstanten für die beiden Wahrheitswerte reserviert) oder
• aus mehreren Groß-/Kleinbuchstaben und Ziffern bestehen, wobei das erste Zeichen keine Ziffer sein darf.

Sonderzeichen, deutsche Umlaute und dergleichen sind nicht erlaubt.

Zulässige Variablen sind also beispielsweise A, x, variable oder Irgendwas. Nicht erlaubt sind hingegen zum Beispiel (abc), t oder a_b.

Bei Eingaben, die nicht als zulässige aussagenlogische Formeln erkannt werden, wird der Hintergrund des Eingabefeldes rötlich eingefärbt. Klickt man auf die Schaltfläche ,,Konvertieren”, wird im unteren Bereich des Fensters eine Meldung angezeigt, die darauf hinweist, was der Eingabe fehlt, um vom Programm als aussagenlogische Formel gewertet zu werden.

Wenn die Einfügemarke hinter einer öffnenden oder schließenden Klammer positioniert wird, werden im Eingabefeld werden zusammengehörende Klammern markiert.

Unterhalb der Schaltflächen für die Junktoren kann man einen von drei Modi auswählen, den das Programm zur Umformung der eingegebenen Formel verwenden soll (die Bezeichnungen sollten ohnehin selbsterklärend sein):

• Einzelschrittmodus: Der Benutzer muss jeden einzelnen Schritt, der durchgeführt werden soll, selbst auswählen (siehe unten).
• Alle Zwischenschritte: Die gesamte Umformung wird automatisch vom Programm durchgeführt. Dabei werden die Regeln von außen nach innen angewandt, das heißt, im Ausdruck $\left(A\:f\:B\right)$ mit f ∈ {∧, ∨, ⊂, ⊃, ⊄, ⊅, ↑, ↓, ≡, ≢} wird zuerst auf den gesamten Ausdruck eine Regel angewandt (beispielsweise die Ersetzung von $\left(A \uparrow B\right)$ durch $\left(\neg A\vee \neg B\right)$); erst dann werden die beiden durch die Funktion verknüpften Formeln auf mögliche Regelanwendungen untersucht, wobei von links nach rechts vorgegangen wird.
• Nur Endergebnis: Für jeden der in Kapitel 2.2 beschriebenen Schritte wird nur jeweils das Endergebnis angegeben, die Zwischenschritte nicht.

Abbildung 2: Ergebnisansicht

Durch Auswahl der Schaltfläche ,,Konvertieren” wird die Ansicht gewechselt (siehe Abbildung 2). Nun sind drei Tabs zu sehen:

• Konvertierung: Hier wird die Umformung der eingegebenen Formel in die äquivalente KNF beziehungsweise DNF durchgeführt. Darüber hinaus werden die so erhaltenen Formeln nach Möglichkeit (des Programms) vereinfacht (siehe Kapitel 3.3 für Details).
• Erklärung: In diesem Tab werden die Schritte, welche im Tab Konvertierung zu sehen sind, im Detail erklärt. Werden im Tab Konvertierung die Zwischenschritte nicht angezeigt, sondern nur die Endergebnisse, so werden hier keine Erklärungen angezeigt.
• Info: In diesem Tab ist eine kurze Information zum Programm zu finden.

Werden alle Zwischenschritte angezeigt, so werden die Funktionssymbole an Stellen, an denen eine Regelanwendung möglich ist, in grüner Farbe angezeigt. Klicken Sie darauf, um die entsprechende Regel anzuwenden. Alle bereits vorhandenen Umformungsschritte ab jener Formel, die angeklickt wird, werden dabei verworfen. Junktoren an Stellen, an denen eine Regel angewandt wurde, um zum nächsten Umformungsschritt zu kommen, werden grau unterlegt.

Im Einzelschrittmodus werden Links, die dem Beginnen eines Schritts, der Anwendung eines Vereinfachungsschrittes beziehungsweise der Transformation der KNF in Klauselform und wieder zurück dienen, in blauer Farbe dargestellt.

Zusammengehörende Klammern werden auch hier markiert, wenn die Einfügemarke hinter einer öffnenden oder schließenden Klammer positioniert wird.

Mit Hilfe des Kontrollkästchens ,,Zwischenschritte anzeigen” kann festgelegt werden, ob alle Zwischenschritte der Umformung dargestellt werden oder nicht. Diese Option kann nicht verändert werden, wenn der Einzelschrittmodus aktiv ist.

Die Änderungen von einem Einzelschritt zum nächsten werden angezeigt, wenn das Kontrollkästchen ,,Änderungen kennzeichnen” aktiviert ist. Werden keine Einzelschritte angezeigt, ist diese Option nicht verfügbar.

Möchte man eine andere Formel eingeben (oder die derzeit verwendete Formel verändern), klickt man einfach auf die Schaltfläche ,,Andere Formel” und kommt zurück zur Eingabemaske.