TabVis verwendet den Tableaukalkül für klassische Aussagenlogik um bool'sche Formeln zu beweisen. Dabei erfolgt die Tableaukonstruktion interaktiv und wird visualisiert. Zusätzlich stellt TabVis auch Methoden für die automatische Beweissuche bereit.
Historisch gesehen wurde der Tableaukalkül unabhängig von Beth(1955), Hintekka(1955) und Schütte(1956) vorgestellt. TabVis benutzt eine Variation der damals vorgestellten Kalküle. Dieser Kalkül wurde 1968 von Raymond M. Smullyan eingeführt und verwendet signierte anstatt normaler Formeln. Abgesehen davon werden wir in der Folge auch eine "einheitliche" Notation für die Tableauregeln verwenden, die ebenfalls von Smullyan vorgeschlagen wurde und sich bei den Korrektheits- und Vollständigkeitsbeweisen als nützlich erweisen wird.
TabVis benutzt den von Smullyan entwickelten Kalkül um Beweise interaktiv aufzubauen. Das angestrebte Ziel des Projekts ist es, Studenten den Einstieg in die klassische Aussagenlogik und Tableaukalküle zu erleichtern.
Der Einfachheit halber werde ich in der Folge die gleichen logischen Symbole verwenden, wie sie auch in TabVis benutzt werden, das sind "-" für die Negation, "v" für oder, "&" für und und "->" für die Implikation.
Der Tableaukalkül basiert auf 8 fundamentalen Eigenschaften der klassischen Logik, die immer gültig sind (das heißt für jede Interpretation). (ab hier werde ich nicht mehr erwähnen, dass wir über klassische Aussagenlogik sprechen; alle Aussagen beziehen sich nur auf diese Logik, wenn es nicht explizit anders gesagt wird).
Bevor wir einen Blick auf die eigentlichen Regeln im Kalkül werfen, werden wir noch den Begriff einer signierten Formel einführen. Syntaktisch ist eine signierte Formel eine Erweiterung einer unsignierten Formel um einen Buchstaben aus {f, t}. (informell steht f für falsch und t für true). Die Schreibweise, wie sie in TabVis verwendet wird ist X : Y, wo X ein Element der Menge {f, t}, und Y eine unsignierte Formel ist. Die Semantik ist wie folgt definiert: Ein signierte Formel X : Y ist genau dann wahr (in einer Interpretation) wenn entweder Y wahr und X t oder Y falsch und X f ist.
Abbildung 1: Tableau Regeln
Wie in Abbildung 1 ersichtlich gibt es konzeptionell 2 Arten von Regeln. Zum ersten Typ gehören die Regeln falsch-oder, wahr-und, falsch-impliziert und beide Negationsregelen. Diese Art von Regeln werden wir von jetzt an als alpha Regeln bezeichnen, wie von Smullyan in der "unified notation" vorgeschlagen. Die Semantik dieser Regeln ist informell die folgende: Die obere signierte Formel ist wahr genau dann, wenn die beiden Unteren wahr sind. Anders gesagt macht jede Interpretation, die die beiden unteren Formeln wahr macht auch die Obere wahr. Die Regeln vom zweiten Typ, die wir beta Regeln nennen, können folgendermaßen beschrieben werden: Die obere signierte Formel ist genau dann wahr, wenn (mindestens) eine der unteren signierten Formeln wahr ist.
Nachdem wir die Regeln für den Tableau Kalkül nun kennen gelernt haben, können wir uns der Beweissuche widmen. Zuerst werden wir einige Definitionen einführen:
Es wurde bis jetzt noch nicht definiert was es heißt eine Regel anzuwenden. Wenn der Knoten auf den eine Regel angewandt wird ein Blatt ist, dann werden die neuen Formeln entsprechend der in Abbildung 1 gezeigten Regeln direkt an ihn angefügt. Eine wichtige Eigenschaft des Tableaukalküls für klassische Aussagenlogik ist allerdings der Don't care Indeterminismus, der sagt, dass es keine Rolle spielt in welcher Reihenfolge die Regeln angewendet werden. Es ist also möglich, dass eine Regel auf einen Tableauknoten angewendet wird, obwohl dieser nicht Blatt seines Astes ist. Es gibt mehrere Möglichkeiten mit diesem Problem umzugehen; im folgenden wird beschrieben wie TabVis mit diesem Problem umgeht: Wenn ein Knoten kein Blatt ist (Ein Tableau kann als Baum angesehen werden, die Begriffe Ast, Blatt, Wurzel sind dementsprechend definiert), ist er Wurzel eines oder mehrerer Subäste. Was nun passiert, wenn eine Regel auf diesen Knoten angewendet wird, ist dass die neuen Knoten an jeden Subast weitergegeben werden, und an deren Enden angehängt werden. Auf diese Art und Weise kann man sicher sein, dass man in jedem Knoten nur einmal eine Regelanwendung durchführen muss. (Abbildung 2 soll diese Vorgehensweise verdeutlichen)
Abbildung 2 zeigt ein Beispiel eines Beweises in TabVis, der das oben beschriebene Prinzip illustriert:
Abbildung 2: Ein Beweis in TabVis
Die Fromel, die wir beweisen wollen ist Y = ((-A)vB)->(A->B). Im Tableaukalkül versuchen wir eine Formel zu beweisen, indem wir ihre Negation widerlegen. Dazu müssen wir die Formel mit f signieren. Wir können uns vorstellen, dass wir mit jeder Regelanwendung neue Eigenschaften hinzufügen, die ein Modell für f : Y haben muss. Jeder Ast stellt einen Teil einer Interpretation dar. Wenn jede dieser Interpretationen einen Widerspruch enthält, und damit alle Äste geschlossen sind, existiert kein Modell für f : Y, also ist Y gültig. Dass ein geschlossenes Tableau tatsächlich eine hinreichende (und notwendige) Bedingung für die Unerfüllbarkeit einer Formel ist werden wir im Abschnitt Korrektheit und Vollständigkeit beweisen. Der nächste Absatz beschreibt den eigentlichen Beweisvorgang:
Abbildung 2 zeigt einen Beweis für die Formel Y. Wir gehen davon aus, dass Y falsch ist, deshalb ist die Formel f : Y an der Wurzel des Tableaus. Wir werden jetzt Schritt für Schritt Regeln auf die einzelnen Knoten des Tableaus anwenden, bis es vollständig ist. Als erstes wenden wir die falsch-impliziert Regel auf den Wurzelknoten an. Diese Regel ist eine alpha Regel. Es werden also die beiden Nachfolger linear an die Wurzel angehängt. Als nächstes wollen wir die Regel für den Knoten anwenden, der mit (2) beschriftet ist. Hier wird die wahr-oder Regel benötigt. Da das eine beta Regel ist, wird der aktuelle Ast in zwei neue Unteräste aufgespaltet, die die Knoten (4) und (5) beinhalten. (Wir hätten auch zuerst die Regel für Knoten (3) anwenden können.) Jetzt wird die Regel für den Knoten (3) angewendet. Dies ist die falsch-impliziert Regel, also wieder eine alpha Regel. Der Ast, der den Knoten (3) enthält teilt sich in mehrere Unteräste. Deshalb müssen alle neu erzeugten Knoten linear zu allen Unterästen von (3) hinzugefügt werden. Nach dieser Operation ist der rechte Ast des Tableaus bereits geschlossen, nur die wahr-negation Regel muss noch angewendet werden, um den zweiten Ast und das Tableau zu schließen, und damit den Beweis zu vollenden.
Der hier skizzierte Beweis ist dem Buch "First Order Logic" von Raymond M. Smullyan entnommen.
Zu zeigen ist, dass wenn ein Tableau für eine signierte Formel geschlossen ist, diese Formel unerfüllbar ist. Der Beweis erfolgt indirekt über Induktion nach der Anzahl der angewendeten Regeln im Tableau. Wir beweisen also die Kontraposition der obigen Aussage: Für jede erfüllbare Formel ist jedes vollständige Tableau offen (im Sinne von nicht geschlossen). Für den Beweis benötigen wir noch eine zusätzliche Definition: Ein Ast eines Tableaus ist wahr unter einer Interpretation v, genau dann wenn jede (signierte) Formel auf diesem Ast von v wahr gemacht wird. Ein Ast der unter irgendeiner Interpretation wahr gemacht wird kann nicht geschlossen sein.
Als erstes werden wir den Fall betrachten, dass im Tableau noch keine Regel angewendet wurde. Das Tableau besteht demnach nur aus dem Wurzelknoten. Die signierte Wurzelformel ist aber laut Annahme erfüllbar, also ist der einzige Ast im Tableau wahr unter einer Interpretation und demnach nicht geschlossen.
Induktionsschritt: Wenn ein Tableau für eine erfüllbare Formel nach n Schritten einen Ast besitzt der wahr unter einer Interpretation v ist, dann besitzt das Tableau nach einer weiteren Regelanwendung immer noch so einen Ast. Wir nehmen also an, dass wir ein Tableau für eine erfüllbare Formel betrachten und nach n Regelanwendungen existiert ein Ast b, der unter einer Interpretation v wahr wird. Wir unterscheiden nun zwei Fälle: Der erste Fall ist, dass die nächste Regelanwendung den Ast b nicht betrifft. In diesem Fall bleibt b natürlich wahr unter v und der Beweis ist vollendet. Im anderen Fall unterscheiden wir welche Regel angewendet wurde. Wenn eine alpha Regel angewendet wurde, werden neue Formeln zum Ast b hinzugefügt und die Prämisse der Regel ist ein Knoten in b. Die fundamentalen Eigenschaften, die wir am Anfang dieses Abschnitts besprochen haben sagen uns, dass wann immer eine Prämisse einer alpha Regel wahr unter der Interpretation v ist, sind auch die Konklusionen wahr unter v. Folglich ist auch der erweiterte Ast b wahr unter v. Dasselbe gilt für die beta Regeln. Die fundamentalen Eigenschaften sagen uns, dass wenn die Prämisse der beta Regel wahr unter v ist, dann ist auch eine der Konklusionen wahr unter v. Daraus folgt, dass einer der beiden aus b entstehenden Äste wahr unter v ist.
Wir haben nun also gezeigt, dass es nicht möglich ist für eine erfüllbare Formel ein geschlossenes Tableau zu konstruieren. Daraus folgt, dass aus der Existenz eines geschlossenen Tableaus die Unerfüllbarkeit der Formel folgt.
Für jede unerfüllbare Formel existiert ein geschlossenes Tableau. Wir werden hier noch mehr zeigen, und zwar dass für jede unerfüllbare Formel jedes vollständige Tableau geschlossen ist. Der Beweis erfolgt wie zuvor indirekt. Wir wollen also zeigen, dass für jedes vollständige Tableau, das einen offenen Ast besitzt gilt: Dieser Ast ist wahr (unter einer Interpretation) und daraus folgt, dass die ursprüngliche Formel erfüllbar ist. (weil sie Teil des Astes ist)
Als erstes notieren wir einige Eigenschaften, die Formelmengen haben müssen wenn sie auf einem offenen Ast liegen:
Wir werden jetzt zeigen, dass für jede Menge mit diesen Eigenschaften eine Interpretation existiert, die alle Formeln in der Menge wahr macht. Im Beweis werden wir nicht nur die Existenz des Modells beweisen, sondern es tatsächlich konstruieren. Dadurch erhalten wir wann immer ein offener Zweig im Tableau für beispielsweise f : B auftritt, ein Gegenmodell für B (also eine Interpretation unter der B falsch wird).
Das Modell für eine Menge mit den geschilderten Eigenschaften wird wie folgt konstruiert:
Wir müssen jetzt noch zeigen, dass diese Interpretation tatsächlich alle Formeln in der Menge wahr macht. Wir verwenden dazu Induktion nach der Formelkomplexität (i.e. die Anzahl der Operatoren in der Formel). Der Induktionsanfang ist in diesem Fall trivial, da Formeln mit Komplexität 0 Atome sind, und die sind in unserer Interpretation nach Definition wahr.
Im Induktionsschritt unterscheiden wir zwei Fälle. Als erstes betrachten wir alpha Formeln. Wir wissen, dass für jede alpha Formel auch die Konklusionen (die wir durch Anwendung der entsprechenden Regel auf diese Formel erhalten) in der Menge sind. Da die Konklusionen eine geringere Komplexität haben als die alpha Formel sind diese per Induktionsannahme wahr in der betrachteten Interpretation. Daraus ergibt sich aber sofort, aufgrund der fundamentalen Eigenschaften, dass auch die alpha Formel wahr sein muss. Im zweiten Fall betrachten wir eine beta Formel. Hier wissen wir, dass eine ihrer Konklusionen in der betrachteten Menge sein muss. Diese ist wiederum nach der Induktionsannahme wahr, woraus folgt, dass auch die beta Formal wahr ist.
Das beendet den Beweis der Vollständigkeit. Bemerkenswert ist, dass die Einführung der "unified notation" uns eine Menge Arbeit erspart hat, weil wir bei den Fallunterscheidungen nur 2 Regeln unterscheiden mussten, während wir anderenfalls hätten 8 unterscheiden müssen.
Wir werden jetzt darauf eingehen wie uns TabVis dabei helfen kann boolesche
Formelen zu beweisen. Zuerst wird die Eingabesprache von TabVis beschrieben,
danach werden alle Funktionen erklärt.
TabVis ist ein Beweissystem für aussagenlogische Formeln; diese Formeln sind also der Input. Es können nur unsignierte Formeln spezifiziert werden. Es wird dann versucht die Gültigkeit der Formel zu beweisen. Das ist aber keine Einschränkung, denn über Eingabe der negierten Formel können alle gewünschten Resultate bewiesen werden (Gültigkeit, Erfüllbarkeit, Unerfüllbarkeit). Die Variablen in den Formeln können aus Großbuchstaben und Ziffern bestehen. Außerdem müssen sie mit einem Großbuchstaben beginnen. (Beispiele für Variablennamen sind also A, S1, SBC123, aber nicht Abc, weil keine Kleinbuchstaben in Variablennamen erlaubt sind). Die Operatoren sind:
Die spezifizierte Formel muss vollständig geklammert sein. Leerzeichen und anderer Whitespace wird komplett ignoriert. Im Folgenden sehen wir eine Grammatik der Inputsprache.
Formula => Simplef | "-"
Simplef | Simplef "&" Simplef | Simplef "v" Simplef |
Simplef "->" Simplef
Simplef => "(" Formula ")" | Atom
Atom => ("A" | ... | "Z")
{"A" | ... | "Z" | "0" | ... | "9"}
Einige Beispiele für gültige Inputformeln sind:
Ungültige Formeln wären:
Nach der Eingabe der zu beweisenden Formel in das Input Eingabefeld startet man den Beweis durch einen Klick auf den "Prove..." Button. In Abbildung 3 ist ein Bild des User Interfaces von TabVis mit Erklärungen zu den einzelnen Komponenten. Wenn die spezifizierte Formel korrekt geparst werden konnte, wird das Wurzelelement des Tableaus in das Tableau Panel gezeichnet. Es enthält die spezifizierte Formel und ist mit f signiert. Wenn die Formel nicht eingelesen werden konnte erscheint eine Fehlermeldung im Output Bereich.
Abbildung 3: Die Funktionen von TabVis
In Abbildung 3 sind die Bereiche des TabVis User Interfaces abgebildet. Das Input Textfeld ist jenes Eingabefeld, in dem die Formeln spezifiziert werden können. Da alle Whitespacezeichen ignoriert werden kann das Layout der Formel sich auch über mehrere Zeilen erstrecken. Im Outputbereich werden Erklärungen zu den einzelnen Schritten während der Tableau Konstruktion angezeigt. Außerdem sind hier auch zusätzliche Informationen nach dem Ende des Beweises ersichtlich (wie zum Beispiel ein Gegenmodell wenn die spezifizierte Formel nicht gültig war). Zusätzlich wird im Outputfenster das Tutorial angezeigt, das Sie durchgehen sollten bevor Sie TabVis benutzen.
Beweise werden in TabVis interaktiv geführt. Das heißt Sie können nachdem die Formel im Tableau Panel angezeigt wird einen Schritt im Beweis durchführen, indem Sie auf den Tableau Knoten, der die Formel enthält klicken. Es wird dann die betreffende Regel für diesen Knoten angewendet und die so neu entstandenen Knoten werden dem Tableau hinzugefügt. Achten Sie darauf, dass Sie tatsächlich auf die Formel innerhalb des Tableau Knotens klicken müssen um die Regelanwendung auszulösen. Wenn sie beispielsweise auf den "derived from ..." Bereich des Knotens drücken wird nichts passieren. In Abbildung 3 wurde bereits eine Regel auf den Wurzelknoten des Tableaus angewendet, deshalb sind die Knoten (2) und (3) bereits im Tableau eingetragen. Wie Sie sehen können wird im Outputfenster angezeigt welche Regel angewendet wurde, und die Regel wird kurz beschrieben. Sie können eine Regel auf einen Knoten nur einmal anwenden. Wir haben bereits im vorigen Abschnitt gesehen, dass eine Regelanwendung jedenfalls ausreicht. Deshalb wird der Knoten in TabVis nach der Regelanwendung durchgestrichen. Außerdem hat es auch keinen Sinn eine Regel auf eine Atomformel (in Abb. 3 enthält der Knoten (3) eine Atomformel) anzuwenden. Bei einem Klick auf diesen Knoten wird nichts passieren. Sie können den interaktiven Beweis fortsetzen, indem Sie auf die neu erzeugten Knoten klicken. die Reihenfolge in der Sie das tun spielt keine Rolle. In Abbildung 3 gibt es nur die Möglichkeit auf den Knoten (2) eine Regel anzuwenden (denn auf Knoten (1) wurde schon eine Regel angewendet und Knoten (3) enthält eine atomare Formel). Nach endlich vielen Anwendungen wird das Tableau vollständig sein. Sie können dann prüfen ob die ursprüngliche Formel gültig war oder nicht.
TabVis stellt außerdem noch einige zusätzliche Funktionen zur Verfügung. Die Funktionen können über die Buttonleiste über dem Tableau Panel benutzt werden. Als erstes betrachten wir die "Undo" Funktion. Wenn Sie eine "Undo" Operation auslösen wird die letzte Regelanwendung rückgängig gemacht. Sie können auf diese Weise verschiedene Reihenfolgen für Regelanwendungen ausprobieren. Das Resultat wird sich zwar nicht unterscheiden, aber die Zahl der erzeugten Tableau Knoten kann von der Anwendungsreihenfolge abhängen. Sie können beliebig viele Schritte rückgängig machen, bis sie den Initialzustand erreichen, in dem nur der Wurzel Tableau Knoten übrig bleibt. Nach einer "Undo" Operation können Sie eine "Redo" Operation ausführen, die den Schritt wiederholt, den sie zuvor rückgängig gemacht haben. Ein "Redo" Operation kann nur unmittelbar nach einer "Undo" Operation ausgeführt werden. Auch hier sind beliebig viele "Redo" Operationen möglich, allerdings nur dann wenn zuvor ebenso viele "Undo" Operationen durchgeführt wurden.
Eine weitere nützliche Funktion von TabVis ist die "Show Entire Proof" Funktion. Sie ermöglicht es sofort (das heißt ohne weitere Interaktion) ein vollständiges Tableau zu erzeugen. Mithilfe dieser Funktion können Sie ein nicht vollständiges Tableau jederzeit vervollständigen. Sie können also einerseits ein vollständiges Tableau sofort erzeugen, nachdem Sie die Formel spezifiziert und den "Prove..." Button gedrückt haben. Andererseits können Sie aber auch einige Regelanwendungen durchführen und dann das bereits erzeugte Tableau vervollständigen lassen. Sie können mit der "Undo" Funktion natürlich auch Schritte rückgängig machen, die während der automatischen Tableaukonstruktion durchgeführt wurden. Dies erleichtert es wiederum verschiedene Konstruktionsreihenfolgen durchzuprobieren.
Mithilfe der "Abandon Proof" Funktion können Sie einen Beweis löschen. Sie können aber auch einfach eine neue Formel eingeben und dann den "Prove..." Button drücken. Achten sie aber darauf, dass in beiden Fällen der alte Beweis unwiederbringlich verloren ist.
Der letzte Button in der Leiste ist der "Tutorial" Button. Wenn Sie diesen
Knopf drücken wird TabVis Sie durch ein interaktives Tutorial führen, indem alle
Funktionen von TabVis, sowie die Grundlagen des Tableaukalküls erklärt werden.
Es wird empfohlen das Tutorial durchzuarbeiten bevor Sie mit TabVis
arbeiten.
Irgendwann wird das Tableau vollständig sein. TabVis schließt dann jeden Ast des Tableaus mit einem Abschlusselement ab. An diesem Abschlusselement ist erkennbar, ob der Ast offen oder geschlossen ist. (Der Knoten wird grün hinterlegt sein, wenn der Ast geschlossen ist und rot anderenfalls.) Wenn Sie auf ein grünes Abschlusselement klicken evaluiert TabVis das Tableau und wird anzeigen, ob die spezifizierte Formel gültig ist oder nicht. (Es kann auch sein, dass das Tableau noch nicht vollständig ist, und trotzdem bereits ein geschlossener Ast existiert, dann wird TabVis darauf hinweisen.) Wenn sie auf ein rotes Abschlusselement klicken, gibt TabVis ein partielles Gegenmodell an, das die spezifizierte Formel falsch macht. Wenn in diesem Gegenmodell nicht alle Variablen vorkommen, dann spielen die Werte der nicht vorkommenden Variablen keine Rolle, und die Werte der angegebenen Variablen sind bereits hinreichend, um die Formel sicher falsch zu machen.
Klicken Sie auf den untern stehenden Button um TabVis zu starten.
Falls Sie Java Script nicht mögen, können sie auch diesen Link benutzen.
Um mit TabVis sinnvoll arbeiten zu können benötigen Sie eine minimale Bildschirmauflösung von 800x600. Wenn Sie eine niedrigere Auflösung verwenden, benutzen Sie bitte die Stand Alone Version von TabVis. Sie können dort nämlich die Größe der Applikation verändern (Sie können die Applikation hier herunterladen)
TabVis wurde mit Java Version 1.4.2 entwickelt und getestet. Tests wurden auf Windows und Linux Plattformen durchgeführt. Die verwendeten Browser waren (Windows: IE 6.0, Mozilla Firefox 1.0.3, Opera 8.0; Linux: Konquerer 3.2, Mozilla ? (Die Version, die auf den meisten ZID Rechnern installiert ist)). Sollten Sie Probleme mit der Ausführung von TabVis unter dem Browser und Betriebssystem Ihrer Wahl haben, wenden Sie sich bitte an mich. Sie können dann auch die Stand Alone Version von TabVis ausprobieren. (Sie können die Applikation hier herunterladen)
Die neuste Version vom TabVis Applet wurde hinsichtlich der Kompatibilität verbessert. Es ist jetzt nur mehr Java Version 1.2.2 nötig, um das Programm korrekt auszuführen.
Sollten Sie nicht sicher sein welche Java Version ihr Browser benutzt, dann klicken Sie hier.
TabVis verwendet den Cup Parser Generator und JLex. Mehr Information zu Cup können Sie hier finden. Natürlich ist auch der Source Code von TabVis verfügbar. Sie können ihn mit dem folgenden Link herunterladen. Die Java Dateien befinden sich in dem jar File, das auch die Stand Alone Version von TabVis enthält.
Außerdem können Sie die Inputfiles für Cup und JLex herunterladen:
Es gibt keinerlei Einschränkung für die Benutzung von TabVis!
TabVis wurde erstellt von Felix Schernhammer. Wenn Sie Kontakt mit mir aufnehmen wollen schreiben Sie bitte an TabVis@gmx.at