Ja, herzlich willkommen.

Ja, wir haben heute im Wesentlichen so noch Reste laden.

Wir haben zwei Dinge nicht fertig gekriegt.

Wir haben noch etliche Dinge zu Ende zu diskutieren über die Semantik der Logik erster Stufe,

insbesondere haben wir noch zu beweisen den harmlosen Teil der Korrespondenz zwischen Modelltheorie und Beweistheorie,

nämlich, dass zumindest mal die Beweistheorie, also unser Fitch-System, korrekt ist bezüglich der Semantik, die wir angegeben haben.

Und zum anderen haben wir ein Unifikationsalgorithmus angeschrieben und den auch schon ausprobiert,

aber wir haben uns nicht davon überzeugt, dass das Ding tatsächlich tut, was es soll.

Und das folgt jetzt.

Es fehlt uns also jetzt noch der Beweis der Terminierung des Unifikationsalgorithmus, gut streng genommen Beweis der Terminierung und der Korrektheit.

Der Beweis der Korrektheit ist, wenn man die Terminierung mal in der Tasche hat, nicht mehr fürchterlich schwer.

Deswegen betone ich hier also in der Überschrift eher die Terminierung.

Ja, ich werde nicht umhin kommen, ihn jetzt noch mal anzuschreiben, damit wir gleich uns auf ihn beziehen können.

Sie brauchen den nicht noch mal abzuschreiben.

Aber Sie haben den, ja, also ich pinsel das jetzt noch mal ab.

Bei der Gelegenheit können wir uns noch mal an ihn erinnern.

Also er besteht aus einer Stapel Umformungsregeln.

Die erste, die hieß Delete.

Die besteht einfach darin, dass wir eine triviale Gleichung x gleich x aus dem System entfernen.

Wir können sie nicht einfach stehen lassen, weil sie nachher nicht unserem Zielformat entspricht,

weil sie eben hier auf der rechten Seite noch mal wieder x enthält.

Also keine Definition von x darstellt, was ja die Definition unseres Begriffs von gelöster Form war.

Dann.

Die nächste hieß Die kommt wie die Komposition.

Das war der Fall, wo wir also links wie rechts eine Vergleichung, also links wie rechts eines Gleichheitszeichens,

den dasselbe Operationssymbol oben liegen haben.

Und da entfernen wir eben schlicht und einfach dieses gemeinsame schon gleiche Operationssymbol

und reduzieren das jetzt also auf die Teilaufgabe, hier diese ganzen Argumenten gleich zu machen.

Dann haben wir den anderen Fall, dass wir eben links und rechts ein Operationssymbol oben liegen haben,

aber eben verschiedene Operationssymbole sagen wir links f rechts g.

Das ist dann nicht unifizierbar.

Das heißt, die Ausgabe ist entsprechend dann nicht unifizierbar, was wir hier durch diesen Bottom andeuten.

Das ist also ein Clash.

Dann gibt es den Fall, dass wir zwar im Prinzip fast das richtige Format erreicht haben,

nur eben verkehrt rum aufgeschrieben, also mit der Variablen rechts.

Da sortieren wir dann eben einfach durch Vertauschen der Gleichung die Variablen nach links.

Allerdings.

Natürlich nur in dem Fall, wo e dieser Ausdruck, der zunächst auf der linken, dann auf der rechten Seite steht,

selbst keine Variable ist, sonst würden wir hier offensichtlich in eine Schleife laufen.

Und dann der eigentlich in jeder Hinsicht schwierigste Fall,

nämlich der, wo wir an sich schon fertig sind, also praktisch eine Variable links stehen haben und rechts einen Term.

Und da gibt es dann zwei Möglichkeiten.

Einmal der, dass x, die Variable, die da als e definiert wird, rechts in e noch vorkommt, also eine freie Variable von e ist,

und aber nicht gleich e, sodass also da vorne unsere Delete-Regel zuschlagen würden.

Und das ist eben der Occurse-Fall.

Occurse heißt Komfort, also das x kommt rechts noch vor.

Und da schlägt also der sogenannte Occurse-Check an und stellt an dieser Stelle fest, dass das System nicht unifizierbar ist.

Und sonst,

sonst sind wir in der Tat an dieser Stelle glücklich fertig.

Wir haben x als etwas definiert, was x selber nicht mehr erwähnt und können diese Definition jetzt im Rest des Gleichungssystems einsetzen.