Ja, herzlich willkommen.

Wir haben ja letzte Woche kennengelernt den Resolutionsalgorithmus für Logik erster Stufe.

Wir haben auch ein Beispiel gesehen. Ich werde jetzt gleich noch zwei Bemerkungen nachreichen

dazu, die insbesondere hoffentlich die Lösung der Aufgaben erleichtern. Und zweitens werden wir

heute sehen, dass dieser Algorithmus tatsächlich vollständig ist, mit anderen Worten. Immer dann,

wenn man ihm eine unerfüllbare Klauselmenge vorwirft, dann terminiert er und sagt auch

korrekterweise unerfüllbar, indem er also dann letztlich die leere Klausel resolviert.

Wie gesagt, ich beginne mit zwei Bemerkungen.

Wir erinnern uns, dass Teil dieser ganzen Prozedur eine auch ansonsten wichtige Normalform war,

die sogenannte Pränexen-Normalform, in der ich also alle Quantoren einer prädikatenlogischen Formel

ganz nach vorne schiebe. Ich schiebe hier noch den Hinweis nach. Wir haben gezeigt Existenz der

Pränexen-Normalform, aber die Pränexen-Normalform ist keineswegs eindeutig. Ich erinnere mal an die

Regeln, die wir da eingeführt hatten. Zum Beispiel in dem Fall, dass wir hier eine Dysjunktion

oberhalb eines Existenzquantors hatten. Das würden wir also umformen in existiert x, phi oder psi,

wobei da die Seitenbedingungen dranhängen, dass x nicht frei in phi vorkommen darf. Ich hatte

gesagt, aber nicht ausdrücklich hingeschrieben, dass wir diese symmetrischen Versionen dieser

Umformungsregeln auch haben. Es könnte ja sein, dass ein Existenzquantor hier links unter der

Dysjunktion liegt. Das heißt, wir haben auch diese Regel hier. Genau so läuft nur, dass eben das phi

jetzt hier rechts von dem Existenzquantor steht. Wir also hier umschreiben zu existiert x,

x, x, x, x, x.psi oder phi unter derselben Seitenbedingungen. Und entsprechend für den allquantor. Wenn wir jetzt sowas hier haben,

sagen wir so eine Formel hier. Für alle x gilt q von x oder es existiert ein y, sodass p von y.

Das mag ja sein. Dann hätten wir hier jetzt zwei verschiedene Umformungen, die wir gemäß diesen

Regeln umformen, die wir gemäß diesen Regeln anwenden könnten. Wir könnten sagen, okay, ich habe hier

links vom Existenzquantor einen Dysjunkt. Gut, den kann ich hier unter den Quantor ziehen. Also existiert y,

dann kommt mein Dysjunkt für alle xq von x und dann kommt das, was vorher auch schon unter dem

Existenzquantor war, nämlich oder p von y. Oder ich sage, okay, hier habe ich meinen allquantor und rechts davon

steht noch ein Dysjunkt, den ziehe ich unter den allquantor. So, im Moment offiziell nach meiner neuen

Konvention über das Scoping von Quantoren hätte ich also hier eine Klammer zumachen müssen.

Also gemeint war hier vorher, dass da der Scope des Quantors zu Ende ist. Das wäre er von alleine nicht.

Von alleine reicht er so weit, wie er kann. Das wäre jetzt bis ans Ende der Formel gewesen.

Und dass wir jetzt den unter den Quantor ziehen, heißt also schlicht und einfach jetzt, dass ich diese

Klammern hier wegnehme. So, und ich bekomme also jetzt für alle xq von x oder existiert yp, y,

wobei jetzt der Scope des Quantors bis dahin reicht. So, hier mache ich weiter. Hier habe ich nämlich

immer noch einen Dysjunkt außerhalb meines allquantors, den kann ich drunter ziehen.

Ich bekomme also existiert x für alle yq von x oder p von y, wobei jetzt beide Quantoren bis ganz ans Ende

reichen. Oder hier kann ich das genauso machen, dieses q von x hier, diesen Dysjunkt kann ich hier

unter den Existenzquantor ziehen, macht für alle x existiert y, sodass q von x oder p von y.

So, wenn ich jetzt rangehe, das zu skolemisieren, dann, ja gut, es ist zwar in beiden Fällen richtig,

damit weiter zu machen, aber es ist wesentlich praktischer, es hier zu tun. Ja, wenn ich hier

nämlich skolemisiere, gut, dann füre ich eine Skolam-Konstante ein. Gut, eigentlich wie immer

eine Skolam-Funktion, die abhängt von allen vorher allquantifizierten Variablen. Und das hier ist der

erste Quantor, es gibt keine vorher allquantifizierten Variablen. Die kriegt also keine Argumente hier,

die Skolam-Funktion. Das macht also für alle x q von x oder p von c für eine Konstante c.

Hier dagegen habe ich vor dem Existenzquantor einen allquantor, das heißt skolemisieren liefert

fast dieselbe Formel für alle x q von x oder und jetzt aber eben p von f von x. Wobei diese

Abhängigkeit des f von dem x, die ich mir da einkaufe, ja ein reines Artefakt der Umformung ist.

In Wirklichkeit liegt die nicht vor, wie wir hier sehen. Das heißt also Pränexenormalfilm

von Bilden und dann Skolemisieren, das kann man mehr oder weniger schlau machen. Und sie dürfen

das also immer, wenn das gefordert ist, schlau machen. Und gelegentlich mal ist es auch nützlich,

so kleine propositionale Tweaks vorher anzuwenden, vielleicht mal die beiden Konjunkte einer