dass die Wissensbasis \( \{\neg A, B\},\{\neg B, C\},\{A, \neg C\},\{A, B, C\} \)
Das entspricht der Formel
\((\neg A \vee B)\wedge (\neg B \vee C)\wedge (A\vee C)\wedge (A\vee B\vee C)\).
die Formel \( A \wedge B \wedge C \) impliziert.
Das heißt es soll gezeigt werden, dass die Formel
\(F \coloneqq (\neg A \vee B)\wedge (\neg B \vee C)\wedge (A\vee C)\wedge (A\vee B\vee C) \to (A\wedge B\wedge C)\)
eine Tautologie ist.
Mittels Resolution kann gezeigt werden, dass eine Klauselmenge unerfüllbar ist, indem die leere Klausel abgeleitet wird.
\(F\) ist genau dann eine Tautologie, wenn \(\neg F\) unerfüllbar ist. Es ist
\(\begin{aligned} & \neg F\\ \equiv & \neg\left((\neg A\vee B)\wedge(\neg B\vee C)\wedge(A\vee C)\wedge(A\vee B\vee C)\to(A\wedge B\wedge C)\right)\\ \equiv & \neg\left(\neg\left((\neg A\vee B)\wedge(\neg B\vee C)\wedge(A\vee C)\wedge(A\vee B\vee C)\right)\vee(A\wedge B\wedge C)\right)\\ \equiv & \left(\left((\neg A\vee B)\wedge(\neg B\vee C)\wedge(A\vee C)\wedge(A\vee B\vee C)\right)\right)\wedge\neg(A\wedge B\wedge C)\\ \equiv & (\neg A\vee B)\wedge(\neg B\vee C)\wedge(A\vee C)\wedge(A\vee B\vee C)\wedge(\neg A\vee\neg B\vee\neg C) \end{aligned}\)
Leite also aus den Klauseln
\( \{\neg A, B\},\{\neg B, C\},\{A, \neg C\},\{A, B, C\}, \{\neg A,\neg B,\neg C\} \)
die leere Klausel ab.
wie komme ich darauf, dass diese Sachen mit "UND" verknüpft sind und nicht mit "ODER"
Mittels Resolution werden aus Klauseln weitere Klauseln abgeleitet. Die Literale innerhalb einer Klausel sind mit "ODER" verknüpft.
