Ja, herzlich willkommen. Wir hatten letztes Mal besprochen die Semantik von Logik erster

Stufe. Da gibt es ein paar lose Enden, damit sind wir also noch nicht fertig. Die werde

ich aber nächste Woche erledigen, um heute nochmal ein kompaktes Thema zu erledigen,

bevor alle nun noch weiter in den Weihnachtsurlaub entschwinden. Ich sehe, die Hälfte ist ohnehin

schon im Weihnachtsurlaub und zwar Unifikation. Ja, Unifikation ist ein,

ziemlich wichtiges Thema in sämtlichen Bereichen der Implementierung von Logik. Insbesondere,

wenn wir noch logische Programmierung im Programm hätten, gut das haben wir nur extra rausgenommen,

dann hätte man auch gleich eine Maschine zur Hand, die eigentlich ständig nichts anderes tut als

unifizieren. Also das ist das, was ein Prolog-Engine zum Beispiel hauptsächlich tut, der läuft durch

die Gegend und unifiziert. Ja, was heißt das? Einmal kurz motivationsmäßig vorweg.

So, wir alle können Gleichungen lösen, so richtig schwere Gleichungen mit Unbekannten,

wie diese hier. Unifikation ist auch Gleichungslösen, aber Gleichungslösen für viel weniger schlaue Leute

als uns, zum Beispiel für einen Computer. So, viel weniger schlaue Leute als wir, die würden

nicht erkennen, dass wenn man da eine 1 einsetzt für dieses x, dass dann 1 plus 7 eben gerade 8

ergibt, sondern die würden sagen, naja, 1 plus 7 ist ja doch eigentlich was völlig anderes als 8,

nämlich 1 plus 7. Und genau auf dem Level werden wir jetzt Gleichungen lösen. Ja, das gibt es dann

mal an lösbaren Gleichungen. So, diese hier können wir zum Beispiel nehmen. Ja gut, die ist arithmetisch

eigentlich viel komplizierter, weil sie so einen großen Lösungsraum hat. So, wir wollen das jetzt

aber so lösen wie unser nicht ganz so schlauer Zeitgenosse von eben. Und das wird der hinkriegen,

ja? Der sieht, ach Mensch, ich kann hier für x 3 einsetzen und für z 8 und dann steht da 3 plus 8

gleich 3 plus 8. Das glaube ich. Ja, gut. Und, okay, also ich meine, das kommt einem, wenn man das jetzt

sieht zunächst mal nicht so schwierig vor. Sobald sich die Terme so ein bisschen tiefer schachteln

als die beiden, die wir da sehen, wird es dann doch irgendwie einen Tacken komplizierter. Es ist

andererseits zum Glück vielleicht keins von diesen tatsächlich beweisbar schwierigen Problemen,

also es ist nicht NP-hard oder sowas. Man kann es in Polynomialzeit lösen. Und wir werden einen

Algorithmus vorführen oder nicht einführen, von dem wir nicht zeigen werden, dass er das in

Polynomialzeit löst. Wir werden genug Mühe haben zu zeigen, dass er terminiert. In der Tat werden

Sie wahrscheinlich das erste Semester, was mich nicht bei einem kleineren Patzer ertappt, beim

Terminationsbeweis dieses Algorithmus. Jetzt mal vorausgesetzt, dass nicht doch noch ein Bug drin

ist. Wir werden nicht zeigen, dass er in Polynomialzeit terminiert, aber man kann zeigen,

dass man das zumindest hinbekommt, ihn so zu tweaken, dass er in Polynomialzeit terminiert.

Trotzdem tut sowas niemand. Also es gibt praktische Algorithmen zur Unifikation. Diese praktischen

Algorithmen laufen alle theoretischen Exponentialzeit. Theoretisch. Gut. Wir haben also irgendwie zu tun

mit Gleichungen. Wenn man sich an die Mittelschule oder Mittelstufe erinnert, an die Mittelschule,

das heißt ja was anderes, Mittelstufe, dann wird man sich erinnern, dass auf die Gleichungen dann

irgendwie relativ bald auch Gleichungssysteme folgten. So und jetzt werden wir uns also in

der Tat hier mit Gleichungssystemen befassen. Fangen also gleich ohne weiteres Geschwafel an

mit einer Definition. Ja, wir müssen also dann zunächst mal sagen, was überhaupt eine Gleichung

ist. So, eine Gleichung ist jetzt erstmal schlicht und einfach ein paar von Termen. Logisch. Eine linke

Seite und eine rechte Seite der Gleichung, jeweils ein Term. Und dann führen wir ein bisschen

Notation ein, damit wir uns bei so einem paar das Richtige denken und also gewissermaßen nicht

vergessen, dass es eine Gleichung ist. Wir würden es eigentlich gerne so schreiben, aber wir wollen

unterscheiden zwischen tatsächlicher syntaktischer Gleichheit, die schon gilt und syntaktischer

Gleichheit, die erst hergestellt werden soll. Bisher, also es kam ja das Gleichseitssymbol

einerseits in Formeln vor. Da meint es natürlich Gleichheit im Modell. Das haben wir in der Semantik

gesehen. Und wenn wir auf der Meta-Ebene Gleichheit verwenden, also in der Diskussion über die Logik,

meinen wir mit Gleichheit immer syntaktische Gleichheit. So und hier so eine Gleichung meint

aber jetzt noch keine syntaktische Gleichung, die schon gilt, sondern eine, die wir erst noch

herstellen wollen. Deswegen packen wir einen Punkt darüber. Ja, da müssen wir sagen, was ein

Gleichungssystem ist. Und ein Gleichungssystem ist eben schlicht und einfach eine Menge von Gleichungen,