Herzlich willkommen. Wir werden heute die zunächst letzte Sitzung zum Thema Aussagenlogik haben, bevor wir uns ab der nächsten Sitzung dem Thema logische Programmierung zuwenden, worauf einige von Ihnen vielleicht schon relativ sehnsüchtig warten.

Was wir heute tun wollen ist zum einen uns weiter mit Normalformen befassen. Wir haben letztes Mal die Negations-Normalform schon angedeutet. Wir sehen uns heute an, wie man die tatsächlich herstellt.

Wir werden weiter übergehen zur konjunktiven Normalform oder sogenannten Klauselform, die eben durchaus gerade für die logische Programmierung auch wichtig ist.

Und wir werden uns ansehen, einen Algorithmus, der uns entscheidet, ob eine gegebene aussagenlogische Formel erfüllbar ist oder nicht.

Das ist ja zunächst mal nichts, was einem vom Hocker haut. Selbstverständlich kann ich entscheiden, ob eine aussagenlogische Formel erfüllbar ist oder nicht.

Ich probiere einfach alle möglichen Wahrheitsbelegungen durch. Das ist offensichtlich kein besonders effizientes Verfahren bzw. ist es auch selbst dann, wenn man, sagen wir mal, gut strukturierte Probleme vorgeworfen kriegt, kein effizientes Verfahren.

Es dauert auf jeden Fall exponentiell lange, alle Wahrheitsbelegungen durchzuprobieren, egal wie das Problem konkret aussieht.

Der Algorithmus, den wir uns ansehen werden, der sogenannte Resolutionsalgorithmus, der wichtig ist sowohl in der logischen Programmierung als auch insbesondere in Theoreenbeweisern, der sieht im Allgemeinen besser aus.

Das heißt, der braucht natürlich im Zweifelsfalle, also in schlechten Fällen ebenfalls exponentiell lange.

Das hat schlicht und einfach damit zu tun, dass das Problem, mit dem man es hier zu tun hat, nun einmal NP-hard ist. Aber in bestimmten guten Fällen liefert er die Antwort sehr schnell.

Das ist genau das, was man eben haben will in solchen Bereichen. Man hat eben dann ein Interesse an Algorithmen, die zwar nicht in allen Fällen schnelle Antworten liefern.

Das ist eben auch beweisbar unmöglich. Aber man bekommt Algorithmen, die zumindest in vielen Fällen, und man hofft, in denen, die in der Praxis tatsächlich auftauchen, die Antwort eben schnell liefern.

Gut. Ja, wir steigen wieder ein bei der Negations-Normalform. Ich erinnere daran an die Definition, Phi ist in NNF,

wenn in Phi Negation nur in einem sehr restringierten Sinne vorkommt, nämlich immer direkt vor Atomen.

Nur direkt vor Atomen vorkommt. Ja, definieren kann man ja vieles. Die Frage ist nun, wie man eine bestimmte Formel in Negations-Normalform bringt.

Nullte Frage davor ist, was heißt das überhaupt?

Wir sagen, ich habe jetzt versprochen, von diesem Phi mal wegzukommen, weil das Phi an der Tafel nicht zu unterscheiden ist von dem Phi und sich außerdem noch ähnlich anhört.

Also, alles, was früher Phi hieß, heißt ab jetzt Phi. Phi wird ja ansonsten hier ja nicht gebraucht. Kreise kommen hier wenige vor.

Also insofern ist der Buchstabe gewissermaßen frei. Den kennt ja nun hoffentlich jeder.

Also, Phi ist eine Negations-Normalform von Phi. Der Dreizag war besser. Also, wer ist für Phi, wer ist für Phi? Also einmal Hand hoch.

Also, wer ist für Phi? Das ist gerade genau die Hälfte. Okay, und wer ist für Phi? Das muss ich jetzt wirklich...

Das ist ja jetzt fast unentschieden. Das ist ja direkt nachzählen hier. Ich probiere mal, wie weit wir damit kommen und am Ende der Vorlesung können wir mal gucken, ob man das lesen kann oder nicht.

Also, Phi ist eine Negations-Normalform von Phi, wenn zwei Dinge gelten. Wenn Phi in NNF ist und ich kann natürlich einfach irgendeine Negations-Normalform nehmen.

Das ist nicht das, was ich meine, sondern Phi soll logisch äquivalent sein zur ursprünglichen Formel Phi. Gut. Und was wir wollen, ist eben eine Negations-Normalform berechnen.

Gut, und wir haben die entscheidenden Äquivalenzen, die man dafür braucht, letzte Woche schon gesehen. Also, die entscheidenden beiden Dinge, die man kennen muss, sind einmal das Gesetz der Doppelnegation, also die Doppelnegation verschwindet.

Und die demorgenschen Gesetze, die mir es gestatten, eine Negation durchzutauschen durch eine Konjunktion bzw. eine Dysjunktion, wobei die entsprechende Konjunktion oder Dysjunktion in eine Dysjunktion oder Konjunktion umkippt.

Und das muss man nur einmal rekursiv richtig machen. Das heißt also, NNF von Phi ist rekursiv definiert durch.

So, und ich mache die, also im Prinzip müsste das so jetzt nach diesen beiden Hinweisen, jeder könne nicht, mache es trotzdem, weil es eine schöne Übung in funktionalen Programmieren ist. Es ist nämlich ausnahmsweise mal keine primitive Rekursion.

Also bisher haben wir ja immer etwas gemacht, das nennt sich eben gerade primitive Rekursion. Das heißt, wir haben eine Grammatik, die besteht in diesem Falle nur aus Atomen nicht und und.

Und wir hangeln uns eins zu eins an der Grammatik lang in der Definition von rekursiven Funktionen. Man wird feststellen, wenn man das hier versucht, kommt man damit nicht durch.

Also ich kann nicht, jedenfalls würde mir das jetzt auch aus dem Stand nicht gelingen, ich kann nicht einfach drei Zeilen in der Definition hinschreiben, die mir jetzt hier die Negations-Normalform definieren.

Nun warum nicht? Naja, es gibt ja, also es gibt zwei uninteressante Fälle, nämlich diejenigen, dass also oben schon eine Konjunktion oder ein Atom liegen, da habe ich nichts weiter zu tun.

In dem Fall ist auch die rekursive Definition offensichtlich. Aber in dem Falle, wo oben eine Negation liegt, kann ich nicht weiterkommen, ohne mir auch anzugucken, was unter der Negation als nächstes kommt.

Das geht also über dieses Schema der primitiven Rekursion, wo ich nun mal den obersten Konstruktor angucke, einen hinaus. Ja, sehen wir uns das jetzt an.

Also wir machen erstmal die einfachen Fälle, also n, n, f von a gleich a, also a als Atom ist bereits in Negations-Normalform, nehme ich einfach, wie es ist.

Ich schreibe die einfachen Fälle immer weiter an derselben Zeile runter. N, n, f von phi und pi.

Naja, gut, da habe ich ja was Legales oben liegen, ja, also keine Verletzung meiner Definition der Negations-Normalform. Ich reiche das einfach nach unten weiter.

Das ist also n, n, f von phi und n, n, f von pi. Ja, dann kommt nochmal oder, da schreibe ich mal einfach nur analog, ja, das funktioniert genauso.

Gut, und die Frage ist jetzt die, also ich habe noch vergessen anzukündigen, Implikation und Biimplikation, ich schreibe mal raus, ja, also raus heißt, ich decode, ich codiere die weg.

Ja, also Implikation ist, also a impliziert, b ist nicht a oder b und Doppelimplikation ist zwei Implikationen.

So, jetzt haben wir alle leichten Fälle abgehakt, und jetzt kommen die schweren Fälle. Also die schweren Fälle sind die, wo oben eine Negation liegt.

Und das heißt, hier steigen wir jetzt einen tiefer in die Formel ein. Wir machen mal davon wiederum den einfachsten Fall, nämlich derjenigen, dass eine Negation oben liegt, aber direkt runter kommt ein Atom.

Das ist ja nun gerade legal, da muss ich nichts weiter machen, das heißt, das ist jetzt nicht a. So, und dann kommen, na ja, noch drei weitere Fälle, nicht?

Wir haben jetzt also in unserer Syntax, ich habe eben gesagt, drei Zeilen, also vier Zeilen wäre richtig gewesen, wir haben in unserer Syntax haben wir und, oder, und nicht, und die Atome, vier Fälle.

Das heißt, hier unterhalb des Nichts kommen jetzt also hier vier verschiedene Fälle ein, einen haben wir abgehakt, der zweite, jetzt einfachste unter den Verbleibenden ist der, dass unter der Negation gleich wieder eine Negation kommt.

Ja gut, da habe ich sofort gewonnen. Ja, also ich nehme das Doppelnegationsgesetz, diese Verletzung meiner Definition des Begriffs der Negationsnormalform, wo hier also ein Negationszeichen vor etwas vorkommt, was selbst kein Atom ist, das kann ich schlicht und einfach wegnehmen.

Das ist also jetzt NNF von Phi. Ja, bleiben zwei Fälle, die dann sich wieder sehr ähnlich sind. Der eine ist der, dass also jetzt unter der Negation als nächstes eine Konjunktion kommt.

So, auch das eine Verletzung meiner Definition, es kommt eine Negation, aber das was drunter ist, ist kein Atom.

Ja, was ich jetzt mache, ist ich schiebe die Negation unter die Konjunktion.

Dabei kippt diese um in eine Disjunktion, nicht nach dem morgenschen Gesetz.