Ja, herzlich willkommen. Sind zur Sitzung von letzter Woche noch Fragen? Sind Sie mit Herrn Hausmann gut klargekommen?

Alles gut. Das ist ja wundervoll, den sollte ich immer schicken. Gut.

Ja, wir haben heute zwei eng zusammenhängende Themen. Wir werden zunächst mal die Theorie der Normalform, die wir ja für Aussagenlogik schon kennengelernt hatten, jetzt erweitern auf Dinge, die spezifisch sind für Logik erster Stufe, die also insbesondere den Umgang mit Quantoren betreffen.

Und wir werden dann aufbauend auf dieser Normalform den Resolutionsalgorithmus, den wir ja auch für Aussagenlogik bereits kennengelernt hatten, erweitern auf Logik erster Stufe.

Das ist also unser großes Ziel für heute. Der Resolutionsalgorithmus ist in Logik erster Stufe anders, muss man deutlich sagen, als im Falle der Aussagenlogik.

Einer, der in der Praxis tatsächlich verwendet wird. Also das gilt eben, wie gesagt, in Aussagenlogik nicht. Kein gängiger Satzsäuber verwendet also ernsthaft das Resolutionsverfahren. Die benutzen andere Dinge.

Dagegen bauen aber viele der modernen und erfolgreichen First-Order-Beweiser, allen voran wohl der Spaßbeweiser, der am MPI in Saarbrücken entwickelt wird, letztlich auf das Resolutionsverfahren für Logik erster Stufe auf, das wir jetzt gleich kennenlernen.

So, wie gesagt, das Ganze verlangt zunächst mal ein paar Normalisierungsschritte auf Formeln und die werden wir uns jetzt in Detail angucken.

Ja, wir fangen an mit der sogenannten Tränexen-Normalform. Die setzt im Grunde das fort, was wir in der Aussagenlogik schon angefangen hatten, wo wir Normalformen im Wesentlichen dadurch gebildet haben, dass wir uns darauf festlegen, wo wir denn gerne welche Operatoren hätten.

Also wir hatten zunächst mal gesagt, Negationen wollen wir ganz unten haben und oberhalb, zum Beispiel in der konjunktiven Normalform, als nächstes dann die Disjunktion, ganz obendrauf die Konjunktion und nun gibt es ja in der Logik erster Stufe außerdem noch diese Quantoren.

Und die Tränexen-Normalform, die tut genau das, was ihr Name sagt, wenn man denn genug Fremdsprache kann, nämlich dass die Quantoren auch einen festgelegten Platz bekommen, ganz am Anfang der Formel.

Das heißt, wir definieren also zunächst mal, was eine Tränexen-Normalform als syntaktisches Format eigentlich ist.

Also eine Tränexen-Normalform werde ich jetzt definieren als eine bestimmte Art Formel.

Ich gebe also gleich die allgemeine Form an, die so eine Tränexen-Normalform hat.

Und zwar beginnt sie mit einem sogenannten Präfix von Quantoren, das heißt also diese QIs, das sind einfach nur Platzhalter für Quantoren, also entweder All- oder Existenzquantoren.

Jeder von denen quantifiziert natürlich eine Variable x1 bis xn und dann kommt irgendeine Formel.

So, nun will ich sicher sein, also das ist eine Formel, wo ganz am Anfang Quantoren kommen.

Ich will jetzt, dass das auch tatsächlich alle Quantoren sind, heißt also, von dieser eingeschlossenen Formel phi hier verlange ich, dass sie quantorenfrei ist.

Also quantorenfrei heißt das, was man denkt, nämlich dass keine Quantoren drin vorkommen.

So, definieren kann man ja nun vieles, klar kann ich mir wünschen, dass die Quantoren alle am Anfang kommen und dass der Mond aus grüben Käse gemacht ist und was auch immer.

Aber man kann diese Normalform tatsächlich herstellen, das heißt es gilt.

Also zu jeder Formel gibt es tatsächlich eine Pränexe nf, die equivalent dazu ist, also wirklich logisch equivalent.

Und die gibt es nicht nur, sondern die kann ich auch berechnen.

Gut, das wird sich aus der Art, wie ich sie herstelle, dann nebenbei ergeben.

Ja, wie mache ich das? Nun, ich mache das wieder durch Umformung, das heißt, das heißt, ich bringe die Formel zunächst mal in Negations-Normalform.

Es müsste letztes Mal erwähnt gewesen sein, wie man in Logik erster Stufe die Negations-Normalform herstellt.

Naja, viel hat man nicht zu tun.

Wenn ich zum Beispiel eine Negation oberhalb eines Quantores habe, wo sie nicht hingehört, dann...

Ja, danke, genau. Das ist Äquivalenz, es existiert nicht viel, genau, vielen Dank.

Das heißt, ich kann so ein Negationszeichen einfach durch ein Quantor durchschieben, dabei kippt der Quantor in sein Duales um.

Und natürlich mache ich das selber mit einem Negationszeichen, was oberhalb eines Existenzquantors steht, der kippt dann in ein Alquantor um.

Das heißt, auf die Weise kann ich dasselbe machen, wie ich in Aussagenlogik schon gemacht habe.

Ich kann also durch jeden Operator die Negation durchschieben, der Operator kippt dabei jeweils in den dualen Operator um.

Und am Ende stehen also alle Negationen ganz innen.

So, das heißt, das sehe ich als schon der Nählicht an.

Also ich habe schon eine Formel in Negations-Normalform und muss jetzt sehen, dass ich die Quantoren, die im Moment irgendwo in der Formel stehen, alle nach vorne kriege.

So, und das mache ich wieder durch geeignete Umformungsregeln, die ich jetzt angebe.

So, was kann denn passieren?

Nun, es kann sein, dass oberhalb eines Quantors noch ein Buhlscher-Operator steht.

So, dieser Buhlscher-Operator ist dann, weil wir ja Negations-Normalform schon hergestellt haben, entweder eine Konjunktion oder eine Dissjunktion.

Negation kann nicht sein, denn die haben wir schon ganz nach innen geschoben, also insbesondere unter die Quantoren.

So, das heißt, es könnte jetzt zum Beispiel sein, dass hier oberhalb eines, sagen wir, Existenzquantors eine Konjunktion kommt mit irgendwas.

So, ich mache jetzt mal nur einen Fall.

Natürlich kann es sein, dass in dieser Konjunktion der Existenzquantor der rechte Konjunkt ist, wie hier. Völlig symmetrisch geht es, wenn der linke Konjunkt ist.

So, gut, jetzt habe ich also dieses Phi hier und ich behaupte, unter einer bestimmten Voraussetzung kann ich das jetzt unter den Quantor ziehen.

Nun, diese Voraussetzung schreibe ich mal ausdrücklich hin, und zwar verlange ich, dass diese quantifizierte Variable X hier, dass die nicht frei vorkommt in dem Phi.

Kann natürlich sein, dass das doch so ist. Es kann sein, dass das Phi das X erwähnt, ohne Weiteres. Und dann ein Quantor kommt, der nochmal über dasselbe X geht.

Aber das ist natürlich kein Problem. Wenn das so ist, dann sind das ja moralisch verschiedene X.

Also das hier ist ein X, das gewissermaßen außen im Scope ist und dann wird der Quantor aufgemacht, der das in diesem Falle verschattet und also über irgendein existierendes X ganz anderer Art redet.

Und ich komme da raus, indem ich das X im Zweifel einfach umbenenne.