Der Tableauxbeweiser

Wir beschränken uns in dieser Aufgabe auf Formeln mit den Junktoren und . Formeln, die auch den Junktor enthalten, müssen zunächst umgeformt werden, was aber nicht Teil der Aufgabe zu sein braucht.
Der Tableaukalkül hat als Eigenschaft, daer nicht wie die Resolution auf Klauseln operiert sondern auf den Formel in ihrer ursprünglichen Syntax. Tableaubeweise sind damit nicht auf einer so maschinennahen abstrakten Ebene und für Menschen leichter lesbar.
Der Kalkül operiert auf markierten Formeln. Eine markierte Formel ist von der Gestalt 0A oder 1A mit A. (Man kann den Tableaukalkül auch auf unmarkierten Formeln definieren. Die Marken dienen nur der Übersichtlichkeit.) Wir unterscheiden drei verschiedene Typen markierter Formeln:

• Typ (elementarer Typ): für .
• Typ (konjunktiver Typ):
• Typ (disjunktiver Typ):

Definition (Tableaux)
Der Tableaukalkül findet sich dargestellt in []. Es sei E eine endliche Menge von markierten Formeln. Ein Tableau für E ist ein Binärbaum mit Beschriftung der Knoten durch markierte Formeln oder durch das Zeichen *, gemäder folgenden rekursiven Definition:

(1)

Ist E={XX}, so ist

ein Tableau für E.

(2)

Ist T ein Tableau für E und ein Pfad von der Wurzel zu einem Blatt, der nirgends mit * markiert ist (offener Pfad) und auf dem ein Knoten mit X vom Typ markiert ist; dann ist auch T' ein Tableau für E, welches durch Verlängern von um ein Blatt mit der Markierung X oder X ensteht.

(3)

Ist T ein Tableau für E und ein offener Pfad von der Wurzel zu einem Blatt, auf dem ein Knoten mit X vom Typ markiert ist; dann ist auch T' ein Tableau für E, welches durch Anhängen zweier Kanten an zu neuen Blättern mit den Markierungen X und X ensteht.

(4)

Ist T ein Tableau für E und ein offener Pfad von der Wurzel zu einem Blatt, auf dem je ein Knoten mit 0A bzw 1A für A markiert ist; dann ist auch T' ein Tableau für E, welches durch Anhängen des neuen Blattes mit der Markierung * an an entsteht.

(5)

Nur die gemä(1)-(4) gebildeten Bäume sind Tableaux für E.

• ein Typ aus zwei Konstruktoren: einer für ein leeres Tableau, einer für einen Knoten mit seinen beiden Nachfolgern und seiner Markierung als Argumente. Ein Blatt wäre dann ein Knoten mit nur leeren Tableaux als Nachfolger.
• ein Typ aus zwei Konstruktoren: einer für ein Blatt und einer für Knoten mit Nachfolgern.
• ein Typ aus drei Konstruktoren: einer für Blätter (0 Söhne), einer für Knoten mit einem Sohn und einer für Knoten mit zwei Söhnen.