SKA ist das SequentialKalkülApplet: ein korrekter und vollständiger interaktiver Beweiser für die klassische Aussagenlogik, der den Sequentialkalkül (auch: LK, Sequenzenkalkül) implementiert.
Die verwendete Version des Sequentialkalküls ist dieselbe wie in der Lehrveranstaltung Theoretische Informatik 1 (185.167). SKA ist als begleitendes Lern-Werkzeug zu dieser Lehrveranstaltung gedacht.
Neben der interaktiven Konstruktion einer Ableitung im Sequentialkalkül hilft SKA auch bei der Interpretation der Ergebnisse, insbesondere beim Finden von Gegenbeispielen aus einem gescheiterten Ableitungsversuch.
SKA ist als Java-Applet implementiert und kann unter http://stud3.tuwien.ac.at/~e0026139/ska/ska.html verwendet werden.
Beim Start zeigt sich SKA wie folgt (je nach verwendetem Betriebssystem können die Bedienelemente unterschiedlich aussehen; die Grundstruktur ist immer gleich):
Das Interface ist in zwei Karteikarten gegliedert, eine für die Ableitung, die andere für Erklärungen und Fehlermeldungen. In der Karteikarte für die Ableitung findet sich eine große weiße Fläche, in der der Ableitungsbaum gezeichnet wird, sowie darunter ein Textfeld und ein Button. In dieses Textfeld kann der abzuleitende Sequent eingegeben werden, bei Betätigung des Buttons beginnt dann die Ableitung, oder, im Falle einer fehlerhaften Eingabe, erscheint eine Fehlermeldung.
Die Eingabe besteht aus zwei möglicherweise leeren Folgen von Formeln, die durch das Sequentzeichen |- getrennt sind. Zwischen zwei Formeln steht jeweils ein Beistrich, Formeln sind vollständig, aber nicht überflüssig geklammert. Sie bestehen aus Atomformeln (Aussagenvariablen), deren Namen mit einem Großbuchstaben beginnen, dem eine beliebige Folge von Groß- und Kleinbuchstaben sowie Ziffern folgt. Sie können durch folgende Junktoren verbunden sein:
| Symbole | Bedeutung |
|---|---|
| & | Konjunktion (und-Verknüpfung) |
| v, | | Disjunktion (oder-Verknüpfung) |
| -> | Implikation |
| -, ~, ! | Negation |
Für Disjunktion und Negation gibt es also mehrere verschiedene Darstellungen, die je nach Geschmack verwendet werden können. Auch eine beliebige Mischung innerhalb eines Sequents ist erlaubt.
Das Format der Eingabe kann auch formal durch eine kontextfreie
Grammatik im EBNF-Format beschrieben werden:
Sequent => [Formel {"," Formel}] "|-" [Formel {"," Formel}]
Formel => Atom | Not Formel | "(" Formel Binop Formel ")"
Atom => ("A" | ... | "Z") {"A" | ... | "Z" | "a" |
... | "z" | "0" | ... | "9"}
Not => "-" | "~" | "!"
Binop => "&" | "v" | "|" | "->"
Leerzeichen sind dabei überall außer innerhalb eines Terminals oder
innerhalb einer Atomformel erlaubt und werden in der Regel
ignoriert. Sie sind an einer Stelle signifikant: Av ist
eine Atomformel, A v ist eine Atomformel gefolgt von einem
Disjunktionssymbol.
Einige Beispiele für syntaktisch korrekte Sequente sind:
Syntaktisch nicht korrekt sind etwa:
Die Eingabe wird durch Betätigung des "Ableiten"-Buttons abgeschlossen. Hat sie nicht die korrekte Form, so wird in der Karteikarte "Erklärung" eine Fehlermeldung angezeigt. Ein "lexical error" steht hier für ein falsches Zeichen in der Eingabe, etwa ein falsches Operatorsymbol oder einen Kleinbuchstaben, der nicht Teil einer Atomformel ist. Die anderen Fehler weisen auf eine falsche Kombination von Terminalsymbolen hin. In der Praxis sind dies meistens Fehler in der Klammerung; die äußersten Klammern um einen zweistelligen Junktor sind zwingend erforderlich. Auch Junktoren, die eigentlich assoziativ sind, müssen eindeutig geklammert sein.
Ist die Eingabe eines Sequents von SKA akzeptiert, wird der Ableitungsversuch gestartet. Der eingegebene Sequent wird unten in der Arbeitsfläche angezeigt; dabei werden statt der Eingabesymbole die "echten" logischen Zeichen verwendet. Weiters werden die beiden Seiten des Sequents als Mengen von Formeln behandelt, Duplikate werden automatisch entfernt. Die Konstruktion des Beweises erfolgt ausschließlich von unten nach oben. Ein gerade angefangener Beweis sieht etwa folgendermaßen aus:
Enthält der Sequent Junktoren, so können die Regeln des Sequentialkalküls auf ihn angewandt werden. SKA ermittelt alle Sequente, die Blätter des Ableitungsbaumes sind: das sind jede, oberhalb derer kein weiterer Sequent mehr steht. In diesen Sequenten wird der äußerste Junktor einer jeden Formel grün hervorgehoben. (Regeln können immer nur auf den äußersten Junktor einer Formel angewendet werden, nie im Inneren der Formel.) Ein Mausklick auf einen dieser Junktoren wendet die entsprechende Ableitungsregel des Sequentialkalküls auf ihn an und stellt den neuen Ableitungsbaum dar.
Solche Regelanwendungen sind immer möglich, solange die Blattsequente Formeln mit Junktoren enthalten. Meistens gibt es mehrere solche Formeln, weswegen die Regeln auch in unterschiedlicher Reihenfolge angewandt werden können. Für den Erfolg oder das Scheitern der Ableitung ist die gewählte Reihenfolge egal, jede endet in endlich vielen Schritten und führt zur selben Aussage bezüglich der Ableitbarkeit des Startsequents. Allerdings kann die Länge einer Ableitung stark von den gewählten Regeln abhängen, und aus unterschiedlichen scheiternden Ableitungsversuchen lassen sich in der Regel unterschiedliche Gegenbeispiele gewinnen.
Um die Übersicht über den zuletzt durchgeführten Schritt der Ableitung zu bewahren, setzt SKA Farben ein. Handelt es sich dabei um die Auflösung eines binären Junktors, so wird sowohl in der Konklusion (unter dem Strich) als auch in den Prämissen (oberhalb des Strichs) die linke Teilformel rosa, die rechte blau hinterlegt. Damit soll auch in größeren Sequenten ersichtlich bleiben, wo die Teilformeln in den Prämissen auftauchen, sowie wo zuletzt eine Regel angewandt wurde. Behandelt der Inferenzschritt einen einstelligen Junktor, so wird dessen Operand rosa dargestellt. In beiden Fällen bleiben die restlichen Formeln des Sequents unverändert und daher auch farblos.
Folgende Abbildung zeigt eine schon etwas weiter fortgeschrittene Ableitung, in der die Teilformeln des letzten Ableitungsschritts farblich hervorgehoben wurden:
Die Anwendung einer oder mehrerer Regeln läßt sich durch einen Klick auf den waagrechten Strich der Inferenz zurücknehmen. Klickt man auf einen solchen Strich, so wird der gesamte Teilbaum oberhalb gelöscht, es kann eine andere Ableitung ausprobiert werden.
Im Lauf der Ableitung tritt auf jedem Ast des Ableitungsbaums einer von zwei Fällen ein: Der oberste Sequent besteht nur noch aus Variablen, aber keine Variable kommt auf beiden Seiten des Sequents vor; dann ist dieser Sequent ein Antiaxiom. Oder aber es gibt eine Formel (die auch Junktoren enthalten darf), die auf beiden Seiten des Sequents vorkommt; in diesem Fall ist dieser Sequent ein Axiom. Beide Fälle werden von SKA erkannt und entsprechend kommentiert. In Axiomen werden zusätzlich auf beiden Seiten die gleichen Formeln unterstrichen, um sie leicht erkennbar zu machen. Enthält ein Axiom noch Formeln mit Junktoren, so kann es noch weiter abgeleitet werden. Dies ist allerdings nie nötig, da die vollständige Zerlegung eines Axioms immer nur auf weitere Axiome führt.
Tritt ein Antiaxiom in der Ableitung auf, so ist der Ableitungsversuch gescheitert. Sind hingegen alle Blätter des Baums Axiome, so war die Ableitung erfolgreich. Die Schlußfolgerungen, die man aus einer gescheiterten bzw. erfolgreichen Ableitung ziehen kann, hängen von der Struktur des untersten Sequents ab. Die Karteikarte "Erklärung" kann zu jeder Zeit angesehen werden, um Aufschluß über den Stand der Ableitung und ihre Bedeutung zu erhalten.