Aufgabe:
In der Vorlesung wurde der Markierungsalgorithmus vorgestellt, mit dem sich effizient testen lässt, ob
eine gegebene Horn-Formel erfülllbar ist. Wir wollen in dieser Aufgabe den Markierungsalgorithmus
benutzen, um die Erfüllbarkeit einer Formel zu testen, die keine Horn-Formel ist.
Gegeben Sei die Formel
ϕ = A ∧ (A → (¬B → C)) ∧ (B → ¬A) ∧ (¬B ∧ C) → D) ∧ (¬D ∨ (E ∧ F)) ∧ (¬E ∨ ¬D ∨ ¬G).
In den folgenden Teilaufgaben bringen wir ϕ zunächst in Implikationsform und konstruieren dann eine
zu ϕ erfüllbarkeitsäquivalente Horn-Formel, auf die wir den Markierungsalgorithmus anwenden können.
a) Formen Sie ϕ äquivalent zu einer Formel ϕ` in Implikationsform um. Begründen Sie, warum die
Formel ϕ´ keine Horn-Formel ist.
