Tableau-Animation - Bernd Baumgarten

B. Baumgarten – Aussagenlogik
Ein einfaches Tableau-Beispiel
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
dunkelblau: noch nicht erledigt
unterlegt: wollen wir jetzt erledigen
grünlich: erledigt
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
B. Baumgarten – Aussagenlogik
1. ¬(ϕ → ψ )
ϕ
¬ψ
¬ ((¬A → (B∨¬C)) → (C→A))
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
Der andere Knoten würde
den Baum breiter machen,
also lieber zu erst den untersten.
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
1. ¬(ϕ → ψ )
ϕ
¬ψ
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
6. ϕ → ψ
¬ϕ | ψ
¬(C→A)
C
¬A
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
¬¬A
B∨¬C
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
¬¬A
B∨¬C
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
5. ¬¬ϕ
ϕ
¬¬A
B∨¬C
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
¬¬A
A
B∨¬C
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
¬¬A
A
B∨¬C
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
¬¬A
A
B∨¬C
8. ϕ ∨ ψ
ϕ |ψ
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
B∨¬C
¬¬A
A
B
¬C
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
B∨¬C
¬¬A
A
B
Tableaubaum fertig (alle Knoten erledigt)
¬C
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
B∨¬C
¬¬A
A
B
abgeschlossenes Blatt
¬C
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
B∨¬C
¬¬A
A
B
abgeschlossenes Blatt
¬C
B. Baumgarten – Aussagenlogik
¬ ((¬A → (B∨¬C)) → (C→A))
¬A → (B∨¬C)
¬(C→A)
C
¬A
B∨¬C
¬¬A
A
B
☺
¬C
Erfüllbar: ja – offenes Blatt
Modell: A → F, B → W, C → W
DNF:
¬A∧B∧C (je 1 Dualklausel pro offenem Blatt)

Download Report