HSG |
|
Wieso verwendet man für die 'semantische Äquivalenz' ein eigenes Zeichen '≡'?
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.
¬(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.
Obige KNF sieht in der Mengenschreibweise folgendermaßen aus:
{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:
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.