Also das Aussagenlogische Tableauverfahren beruht doch auf der Disjunktiven Normalform. Um einen Tableau Beweis zu führen, negiere ich die Formel und führe die Tableau Expansion durch. Habe ich in jedem Zweig abgeschlossen, habe ich gezeigt, dass die eigentliche Formel eine Tautologie ist. Das ist dann ein Widerlegungsbeweis.

Warum kann ich das ganze nicht als direkten Beweis durchführen. Undzwar mit der KNF anstelle der DNF. Also nehme ich die Formel, führe die Tableau Expansion mit den Ersetzungsregeln der KNF durch und wenn ich in jedem Zweig zum Abschluss komme, dann habe ich gezeigt, dass die Formel eine Tautologie ist.

Frage: Ist das möglich? Und wenn ja, warum steht dazu kein Hinweis in den Folien? Wenn nein, warum nicht?

Also das Aussagenlogische Tableauverfahren beruht doch auf der Disjunktiven Normalform.

Hm, eigentlich nicht. Kann es sein, dass du die Algorithmen zum
Herstellen der Klauselnormalform (bzw. der dualen Klauselnormal-
form) mit dem Tableau verwechselst (die Regeln auf Folie 4-62
sehen denen auf 5-7 nämlich zum Verwechseln ähnlich [img]http://www.fb18.de/gfx/28.gif[/img])?

Beides braucht man nämlich nicht: Wenn die Formel in KNF ist,
kannst du mit bloßem Auge erkennen, ob du's mit einer Tautologie
zutun hast (und zwar genau dann, wenn alle Klauseln tautologisch
sind).

Die DNF hilft umgekehrt bei der Entscheidung, ob eine erfüllbare
Formel vorliegt (genau dann, wenn eine der dualen Klauseln
erfüllbar ist).