Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ja, also nochmal herzlich willkommen. Ich erinnere an den Algorithmus, den wir letztes Mal eingeführt

haben, den Resolutionsalgorithmus für Logik erster Stufe. Er basiert im Wesentlichen einzig und

allein auf folgende Regel. Sie sah fast so aus wie die Regel für Resolution in propositionaler

Logik. Mit dem einen Unterschied, dass wir hier mehrere Literale in einer Klausel eventuell zu

einem identifizieren, indem wir was einsetzen, was die gleich macht. Und zum anderen indem wir

eben unifizieren, also wir können diese Literale was einsetzen, das konnten wir ja in Aussagenlogik

nicht. Und zwar unifizieren wir hier diese N positiven Literale mit dem einen negativen hier

und schließen dann C Sigma, D Sigma. Also das zerlegt das Ganze in zwei Schritte. Also

erstens wir setzen da ein, naja in drei Schritte im Grunde. Also erstens wir setzen hier gemäß

Sigma ein, nicht? So haben wir das letztes Mal aufgedröselt. Zweitens, die werden dann alle

gleich, also können wir einen draus machen. Und drittens machen wir dann ganz normale Aussagenlogische

Resolution, weil nämlich dieser eine dann gleich dem da ist, können wir sie beide streichen und C

und D zusammenschmeißen, natürlich unter Anwendung dieser Substitution Sigma. So und das hieß als

Regel RIF wie Resolution with Implicit Factoring, wobei Implicit Factoring sich darauf bezieht,

dass wir eben gleichzeitig diese A1 bis AN noch zusammenfassen. So, dann fragt man sich zwei Dinge.

Erstens, wieso muss das so kompliziert sein? Wieso reicht es nicht da ein einziges positives

Literal zu nehmen? Na ja, man sieht ein schnelles Gegenbeispiel, ja also. Also ein schnelles

Gegenbeispiel, was also zeigt, dass wir diese Faktorisierung, also dieses Identifizieren von

Literalen tatsächlich brauchen, nehmen wir mal diese Klausel hier P von X und P von Y.

Vorgelesen heißt das, für alle X und Y gilt P von X oder P von Y. Naja, das ist natürlich

irgendwo Blödsinn, ja das könnten wir vereinfachen können zu nur P von X, aber nun steht es nun mal so

da. Kann ja auch irgendwie mal so rauskommen. Und hier dasselbe nochmal in Negativ. So, also das

ist offensichtlich ein Widerspruch, ja da steht auf der einen Seite alle X erfüllen P von X,

auf der anderen Seite steht alle X erfüllen nicht P von X, ja auch wenn die X nur zufällig

rechts Z und W heißen. So, wenn wir das jetzt ohne Faktorisierung resolvieren wollen, was passiert

dann nun? Wir können natürlich immer hier einen Positiven mit einem Negativen resolvieren. Was

rauskommt ist eine Trivialität, nämlich P X oder P von, nicht P von irgendwas, ja also es hilft nicht

viel. Also wenn wir das einmal machen, dann einfach nur per Resolution, also ohne Faktorisierung jetzt

mit, also müsste hier die variablen Namen alle Gruß schreiben, der Klarheit halber. So, jetzt hier

zum Beispiel mit Sigma Z gleich Y, dann könnten wir also die beiden hier streichen, dann käme da

raus P X Komma nicht P von W. Gut, dann man sieht, dass man nicht zum Schluss kommt, ja das sind alles

Klauseln mit nur zwei Literalen, die wir da rauskriegen, ja und wenn wir Klauseln mit zwei

Literalen resolvieren, die immer so wie es hier bleibt, nicht? Ja, verschieden sind, also die X und

W, zum Beispiel, das wird immer verschieden bleiben. Ja, könnte auch mal, also die Literale zumindest

sind verschieden, X und W könnten auch gleich werden, wenn ich es einsetze. Ich sehe, dass ich

nicht drüber hinauskomme, da einfach immer Klauseln mit zwei Literalen zu haben, ja, da kann ich also

resolvieren, wie ich will. Nicht dagegen, mit RIF habe ich das sofort weg. So, und da sieht man

gleichzeitig, warum es reicht, nur auf einer Seite die Literale zu duplizieren. Man fragt sich ja,

wenn man die Regel sieht, warum sind nicht auch mehrere nicht Bs da, ja. So, und das kann man aber

hiermit schon ableiten. Also mit RIF, was kann ich machen? Ich kann, ich kann X auf Z abbilden,

also substituieren und Y ebenfalls, ja, dann habe ich diese beiden positiven und den einen negativen

hier gleich gemacht, dann kommt raus, na, die verschwinden alle, übrig bleibt der da, nicht P von W.

Ja, und dann kann ich das noch mal machen. Ich habe die alten Klauseln ja immer noch, das heißt,

ich kann noch mal hier einsetzen, jetzt sagen wir mal, wenn man eine neue Substitution sieht,

sigma 2X gleich W und sigma 2Y auch gleich W, dann werden jetzt hier alle drei gleich, also P von W,

P von W, P von W, das heißt, da kann ich jetzt resolvieren und kriege die leere Klausel raus,

bleibt kann da mehr über. So, das heißt, was wir hier praktisch sehen und das können wir jetzt natürlich auch formal in der Allgemeinheit

durchziehen, aber das erhält auch nicht weiter, deswegen schreiben wir es einfach hin. Also ich sage,

ableitbar ist also, also heißt, so wie wir in diesem Beispiel gesehen haben, folgende verallgemeinerte Version der Regel.