Tableau-Verfahren auch Beweis für Erfüllbarkeit (ohne gleichzeitig Tautologie)

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Tableau-Verfahren auch Beweis für Erfüllbarkeit (ohne gleichzeitig Tautologie)
Hallo,

ich habe eine Frage, an der ich heute den ganzen Tag rumgegrübelt habe, ist vielleicht ein Denkfehler???
Beim Tableau-Verfahren (nehmen wir die Aussagenlogik) wird die ursprüngliche Formel oder Formelmenge negiert und dann versucht, ein Widerspruch zu dieser negierten Form abzuleiten. Sind alle Zweig des Tableau-Baum abgeschlossen, ist der Beweis gelungen und die Ausgangsformel ist als Tautologie bewiesen. O.K. Aber was ist, wenn es gleichzeitig Zweige in einem Tableau gibt, wo die einen abgeschlossen sind, die anderen jedoch nicht (und auch nicht abschließbar, d.h. hier ist kein Widerspruch ableitbar ist). Die Formel ist dann natürlich keine Tautologie, aber ist sie nicht erfüllbar? Der eine Zweig, der abgeschlossen ist, zeigt die Belegung, die die Ausgangsformel erfüllt, der andere Zweig, der nicht abschließbar ist, zeigt eine Belegung, die die Ausgangsformel nicht erfüllt. Aber wenn das so ist, warum finde ich dann überall nur, dass der Tableau Beweis ein Beweis zur Tautologie ist; er müsste dann ja auch ein Beweis für die Erfüllbarkeit einer Formel sein, in obig beschriebenem Fall wäre das dann so, die Formel ist erfüllbar, aber keine Tautologie. Ich denke nur, dass das falsch ist, da ich das nirgendwo lesen konnte. Mache ich einen Denkfehler, wenn ja welchen?
Oder ist der Tableau Beweis tatsächlich beides, Beweis für Tautologien und auch für Erfüllbarkeit, d.h. wenn ich nur Erfüllbarkeit beweisen wollte, könnte ich dann ja aufhören, sobald ich einen Zweig abgeschlossen habe, die anderen Zweige interessieren dann nicht mehr.
Schöne Grüße

acey