Und vor allem Aufgaben drin, die Sie noch nicht lösen können, weil von einem Tablokalkyl

die Rede ist, den wir noch nicht mal in dieser Sitzung, sondern in der nächsten Sitzung

kennenlernen.

Wobei die nächste Sitzung nicht Montag, sondern, nee Moment, wie rum jetzt?

Doch, die nächste Sitzung ist Montag, genau, der Donnerstag nächste Woche fällt aus,

aber nicht der Montag.

Also, Tablokalkyl ist Gegenstand von Aufgabe 1, 3 und 4, denn wie gesagt erst nächsten

Montag.

Aufgabe 2 kann man größtenteils jetzt schon lösen, sofern man in Gleun war, und wenn

nicht dann nach der heutigen Sitzung.

Also Resolutionsalgorithmus machen wir jetzt nochmal.

Und wir machen auch, hoffentlich, DPLL.

Das ist einfach so ein Ausprobieren.

Das meiste ist einfach Ausprobieren, also auch hier Aufgabe 1 ist einfach ganz konkret

mal Anwendung dieses Tablokalkyls, damit man ein Gefühl dafür kriegt, wie die Dinger funktionieren.

Aufgabe 3 ist so ein Metabeweis über ein Tablokalkyl und, achso, nee, Aufgabe 4 kann man jetzt

auch schon lösen, mit der kann man geradezu anfangen.

Aufgabe 4 ist was rein Semantisches über konjunktive Normalformen.

Und zwar ist das was, was tatsächlich positive Logik heißt, das habe ich jetzt nicht erfunden,

was positive Logik ist, kann man komplizierter definieren, aber wenn man konjunktive Normalformen

vor sich hat, heißt das schlicht und einfach, es enthält keine Negation.

Und auch sonst kann man sagen, es enthält einfach keine Negation.

Das heißt, eine Klausel ist dann einfach eine Dysjunktion von Atomen und eine konjunktive

Normalform eine Konjunktion solcher Klausel.

Und hier soll charakterisiert werden, ja, nicht Erfüllbarkeit, also Erfüllbarkeit von

solchen positiven Formeln ist natürlich was sehr Langweiliges.

Ich setze vorsichtshalber mal alle Atome auf wahr, dann ist meine Formel erfüllt.

Das ist jetzt keine interessante Frage mit der Erfüllbarkeit.

Wenn eine Logik eben keine Negation hat, dann kann ich auch nicht logische Folgerungen auf

Erfüllbarkeit reduzieren, indem ich eine Formel negiere und auf die andere Seite schiebe.

Das geht dann eben nicht mehr.

Das heißt, da muss man wirklich logische Folgerungen sich angucken, wenn man was Interessantes

haben will.

Und genau diese logische Folgerung, die soll hier halt charakterisiert werden, ja, das

ist, naja, also, bzw. ist die Charakterisierung hier angegeben.

Es gibt also eine offensichtliche Situation, in der eine solche positive CNF aus einer

anderen Folch, nämlich dann, wenn ich jede ihrer Klauseln, also jede Klausel der Formel,

die hier folgt, schon praktisch hier links vorhanden ist, ok, eventuell mit weniger Atomnöse.

Also, zum Beispiel, wenn ich, also bei Klauseln ist es ja so, dass die kleinen die großen

implizieren.

Also, wenn ich A habe, dann ist das stärker als A oder B.

Also, es impliziert eben A oder B.

Je größer eine Klausel ist, umso schwächer ist sie.

Das heißt also, ich finde, wenn das hier so ist, ja, dann, gut, das muss man natürlich

auch zeigen, aber es ist relativ klar, dass also die Regel, dass das die Implikation von

rechts nach links gilt.

Das heißt, wenn jede Klausel hier rechts größer als eine hier links ist, dann ist das

wohl eine logische Folgerung, aber man soll eben zeigen, dass auch das Umgekehrte gilt.

Und da muss man sich das eben semantisch überlegen.

Da muss man tatsächlich mal Wahrheitsbelegungen angeben.