Semantische Äquivalenz

• Definition Implikation α → β ≡ ¬α ∨ β
• Definition logische Äquivalenz α ↔ β ≡ β → α ∧ α → β
• De Morgan ¬ (α ∨ β) ≡ ¬α ∧ ¬β
• De Morgan ¬ (α ∧ β) ≡ ¬α ∨ ¬β
• Distributivität α ∨ ( β ∧ γ ) ≡ ( α ∨ β ) ∧ ( α ∨ γ )
• Distributivität α ∧ ( β ∨ γ ) ≡ ( α ∧ β ) ∨ ( α ∧ γ )
• Idempotenz α ∨ α ≡ α
• Idempotenz α ∧ α ≡ α
• Kommutativität α ∨ β ≡ β ∨ α
• Kommutativität α ∧ β ≡ β ∧ α
• Assoziativität ( α ∨ β ) ∨ γ ≡ α ∨ ( β ∨ γ )
• Assoziativität ( α ∧ β ) ∧ γ ≡ α ∧ ( β ∧ γ )
• Absorption α ∨ ( α ∧ β ) ≡ α
• Absorption α ∧ ( α ∨ β ) ≡ α
• Doppelte Negation ¬ ¬ α ≡ α

Wieso verwendet man für die 'semantische Äquivalenz' ein eigenes Zeichen '≡'?

Konjunktive Normalform

Eine Formel der Form

(A ∨ ¬B ∨ C) ∧ (D ∨ E) ∧ ... ∧ (¬V ∨ ¬X ∨ Y)

ist in der konjunktiven Normalform. Dabei sind A,B,C,.. aussagenlogische Variablen. D bezeichnet man als positives Literal, ¬V als negatives Literal.

Transformation auf KNF

• Ersetze alle Äquivalenzen α ↔ β durch (β → α) ∧ (α → β).
• Ersetze alle Implikationen α → β durch ¬α ∨ β.
• Verschiebe die Negationen bis zu den Variablen.
• Entferne doppelte Negationen.
• Transformiere auf KNF durch Ausmultiplizieren.

Beispiel

¬(A∨B)↔C
(¬(A∨B)→C)∧(C→¬(A∨B))
(¬¬(A∨B)∨C)∧(¬C∨¬(A∨B))
((A∨B)∨C)∧(¬C∨(¬A∧¬B))
(A∨B∨C) ∧ (¬C∨¬A) ∧ (¬C∨¬B)
(A∨B∨C) ∧ (¬A∨¬C) ∧ (¬B∨¬C) KNF

Programm zur Ermittlung von Normalformen, Wahrheitstabellen, .. von Christian Gottschall.

{A,B,C}, {¬A,¬C}, {¬B,¬C}

A B C | A∨B ¬(A∨B) ¬(A∨B)↔C  A∨B∨C  ¬A∨¬C  ¬B∨¬C  (A∨B∨C)∧(¬A∨¬C)∧(¬B∨¬C)
------+------------------------------------------------------------------------------
0 0 0 |  0      1        0        0       1       1                0
0 0 1 |  0      1        1        1       1       1                1
0 1 0 |  1      0        1        1       1       1                1
0 1 1 |  1      0        0        1       1       0                0
1 0 0 |  1      0        1        1       1       1                1
1 0 1 |  1      0        0        1       0       1                0
1 1 0 |  1      0        1        1       1       1                1
1 1 1 |  1      0        0        1       0       0                0

Zunächst ist an der Wahrheitstabelle abzulesen, dass die oben ermittelte KNF semantisch äquivalent zur Ausgangsformel ist.

Hat man die Wahrheitstabelle, so kann man auf folgende formale Art eine KNF erhalten:

• Für jede Zeile, in der die Formel 0 ergibt, erstellt man eine Disjunktion aus allen Eingabevariablen oder ihrer Negation. Ist eine Variable 0, so nimmt man die Variable, ist sie 1, so nimmt man die Negation der Variablen. In obigem Beispiel erhält man so für die 4.Zeile A∨¬B∨¬C.
• Die so erhaltenen Klauseln werden nun konjunktiv verknüpft.
  Im Beispiel: KNF = (A∨B∨C) ∧ (A∨¬B∨¬C) ∧ (¬A∨B∨¬C) ∧ (¬A∨¬B∨¬C)

Da die Disjunktionen so konstruiert sind, dass sie nur in 'ihrer' Zeile 0 werden und sonst immer 1 sind, ergibt sich die semantische Äquivalenz zur Ausgangsfunktion. Interessant ist, dass im Beispiel die aus der Wertetabelle erstellte KNF komplizierter als die 'berechnete' ist. Man sieht also, dass eine KNF keineswegs eindeutig ist.

Es ist im Allgemeinen nicht sinnvoll, eine KNF über eine Wertetabelle zu ermitteln, weil der Aufwand bei vielen Eingangsvariablen sehr groß wird. Außerdem, was interessiert die KNF, wenn ich die Wertetabelle habe. Mit der Wertetabelle weiß man sowieso alles über die Formel. Dann erübrigt sich ein maschineller Beweis, für den die KNF gebraucht wird.

Links

• konjunktive Normalform - wikipedia