Du befindest dich hier: Aussagenlogik

Semantische Tableaux

(Aussagenlogik Kapitel 8)

Wir haben bereits im letzten Kapitel 3 aussagenlogische Beweisverfahren kurz dargestellt. Nun wollen wie den Tableaukalkül (auch "Beth-Kalkül" oder "Baumkalkül" genannt) genauer betrachten.

Der Tableaukalkül ist ein semantisch motiviertes Entscheidungsverfahren für die Gültigkeit und Erfüllbarkeit von Formeln. Er formalisiert den Vorgang, ein Modell für eine Formel γ anzugeben und basiert auf folgender Idee:

1. Die Zerlegung einer Formel wird als Baum dargestellt: Konjunktionen werden etwa als linearer Ast, Disjunktionen durch eine Verzweigung ausgedrückt.
2. Die Äste des Baumes repräsentieren mögliche Modelle der Formel: befinden sich auf einem Ast ein Atom und seine Negation, ist dieser unerfüllbar und repräsentiert kein Modell.

Um diese vage Beschreibung zu konkretisieren,

• werden wir im nächsten Kapitel eine vereinfachte Version des Tableaukalküls für aussagenlogische Formeln in Negationsnormalform vorstellen.
• Anschließend kann das Erstellen eines semantischen Tableau interaktiv geübt werden.

• zurück zu Die Resolution
• zum Seitenanfang
• weiter zu Ein Tableaukalkül für Formeln in Negationsnormalform

. .