Eine Suchtechnik für Beweise und Erfüllbarkeitstests, die logische Formeln schrittweise entlang eines Baumes (das Tableau oder Wahrheitbaum) in Bestandteile zerlegt, Zweige mit Widersprüchen schließt und so entweder aus einem offenen Zweig ein Gegenmodell konstruiert oder bei Schließen aller Zweige Gültigkeit nachweist.

Prinzip

Syntaktische Zerlegungsregeln auf Formeln anwenden, um mögliche Belegungen oder Modelle zu explorieren: Konjunktionen, Disjunktionen, Quantoren und modale Operatoren gemäß Regelmengen zerlegen, Zweigbedingungen verfolgen und Abschlussregeln sowie Schleifen‑ oder Fairnesskontrollen einsetzen, um gegebenenfalls Termination zu sichern.

Demonstration

Für die aussagenlogische Ebene beginnt man mit der Negation der zu beweisenden Formel und baut ein Tableau: Disjunktionen werden in alternative Zweige gespalten, Konjunktionen auf demselben Zweig hinzugefügt und ein Zweig als geschlossen markiert, wenn er sowohl p als auch nicht p enthält. Ein offener saturierter Zweig liefert eine erfüllende Belegung, sodass Un erfüllbarkeit durch das Schließen aller Zweige belegt ist.

Fehlanwendung

Einen naiven Prädikaten‑Tableau ohne Blocking, Loop‑Checking oder Mechanismen zur Behandlung unendlicher Zweige laufen zu lassen und dies als Entscheidbarkeitsverfahren auszugeben; oder Abschlussbedingungen falsch zu handhaben (z. B. globale Beschränkungen in modalen Tableaus zu ignorieren), was zu falschen Ergebnissen führt.

Konsequenz

Tableau‑Methoden liefern konstruktive Beweise oder Gegenmodelle, lassen sich leicht an viele Logiken anpassen (modal, temporal, Beschreibungssprachen) und bilden die Grundlage zahlreicher automatischer Beweiser und Erfüllbarkeitsprüfer; die praktische Effizienz hängt von Regelreihenfolge und Zweigverwaltung ab.

Umkehrung

Ersetzt man die Tableau‑Suche durch ein Widerlegungs‑Kalkül wie Resolution oder Sequenzen, verändert sich die Suchstruktur von baumbasierter Modellerzeugung zu Klauselmanipulation oder zielgerichteter Schnittelimination und es erfolgt ein Tausch zwischen Modellgewinnung und anderen Komplexitäts‑/Speicherverhalten.

Abgrenzung

Gilt für klassische und viele nichtklassische Logiken, doch erfordern Vollständigkeit und Termination logisch spezifische Regelmengen und mitunter Blocking oder Fairnessstrategien; die Methode garantiert nicht automatisch polynomiale Ressourcen und kann exponentiell viele Zweige erzeugen.

Semantische Spannung

Tableaus betonen lokale syntaktische Zerlegung und explizite Modellerzeugung, was in Konkurrenz zu globalen Methoden wie Resolution oder SMT‑Solvern steht, die Klauseln und Constraints transformieren und kombinieren; die Spannung liegt zwischen Modellextraktion und klauselorientierter Inferenzeffizienz.

Synthese

Die Tableau‑Methode ist eine systematische baumbasierte syntaktische Suche, die Formeln so zerlegt, dass entweder eine erfüllende Belegung konstruiert oder alle Möglichkeiten geschlossen werden; ihre Anpassungsfähigkeit an viele Logiken und ihr konstruktiver Charakter machen sie praktisch, wobei Terminierungsfragen und Verzweigungs‑Komplexität zu beachten sind.