Ja, herzlich willkommen.

Ja, für heute steht auf dem Programm Unifikation.

Ja, Unifikation ist im Wesentlichen Gleichungslösen ohne Semantik.

Also ich löse Gleichungen, von denen ich nicht weiß, was sie bedeuten.

Was meine ich damit?

Nun, also hier haben wir eine Gleichung, die wir vielleicht mal lösen wollen,

könnten oder auch nicht nach dem x plus drei gleich fünf.

Gut, wir können diese Gleichung offensichtlich lösen.

Jeder wird in der Lage sein zu sagen, haha, ich habe hier die Lösung x ist gleich zwei.

So, gut gemacht, aber noch nicht verrechnet.

Ja, was muss ich wissen, um diese Gleichung zu lösen?

Nun, ich muss irgendwie verstehen, was das Pluszeichen und die drei und die fünf heißen.

Also erstmal so, wenn ich das nicht weiß, einfach nur durch Einsetzen, wenn ich x gleich zwei einsetze,

steht da zwei plus drei gleich fünf.

Ich weiß nicht, ob das stimmt oder nicht, es sei denn, ich weiß eben Bescheid über Zahlen.

Hier haben wir eine etwas andere Gleichung.

Mit Dingen, die ich absichtlich so gewählt habe, dass wir eben nicht wissen, was sie heißen sollen, f und g.

Ich schreibe hin f von g von z gleich f von y.

Nun kann ich dafür eine Lösung angeben.

Nun, natürlich kann ich das. Ich kann als Lösung angeben, y ist gleich g von x.

Wenn ich das einsetze, werden ganz sicher die beiden Seiten gleich und ich muss nicht wissen, was f und g tun.

Und genau das hier, das ist also, wie gesagt, lösen mit Semantik und das hier, das hier ist Unifikation.

So wird man ja sagen, okay, also Unifikation ist ja offensichtlich was ziemlich Triviales.

Nun ja, und in der Tat hat sich dann auf längere Sicht gezeigt, dass Unifikation im informatischen Sinne einfach ist.

Das heißt, ich kann sie in Polynomialzeit lösen.

Merkwürdigerweise tut das keiner.

Das ist so einer der Fälle, wo es also einen bekannten Polynomiellen Algorithmus gibt.

Aber alle nehmen trotzdem den Exponentiellen.

Also es ist nicht wirklich ein völlig Triviales Problem.

Es ist nur in dem Sinne Trivial, wie lineares Programmieren Trivial ist.

Lineares Programmieren weiß man auch seit den 80ern, also das Lösen von polyhedralen Ungleichungen.

Wenn ich also Systeme linearer Ungleichungen habe und wissen will, ob die lösbar sind,

das kann ich also oder sie sogar lösen, das kann ich im Prinzip in Polynomialzeit.

Das macht aber auch keiner.

Es nehmen trotzdem alle den Simplex-Algorithmus, der exponentiell lange dauert.

Und auch von linearer Programmierung würde man also nur bedingt sagen, es handele sich um ein Triviales Problem.

So, also das Problem, das wollen wir zunächst mal nicht gleich lösen,

sondern überhaupt erst mal definieren, was es denn eigentlich formal als Problem ist.

Das heißt, jetzt kommt erst mal wieder so ein Stapel Definitionen.

Wir machen aber auch gleich noch Beispiele.

Ja, so zunächst mal, wenn wir also offenbar von Gleichungslösen reden wollen,

dann sollten wir mal definieren, was eine Gleichung ist und wie wir sie schreiben.

Wir schreiben eine Gleichung so, wie sie da jetzt steht, also E gleich D mit so einem Punkt über dem Gleichheitszeichen.

Der Punkt ist dazu da, nun diese Gleichung als Problem von echten Gleichungen,

die nun, sagen wir mal, insbesondere syntaktisch gelten,

zwischen zwei tatsächlich wörtlich gleichen Termen zu unterscheiden.

Also, Punkt drüber heißt immer, das ist etwas, was wir lösen müssen.

So, und formal ist so eine Gleichung schlicht und einfach ein Paar von Termen.

Linke Seite E, rechte Seite D.

Und diese Schreibweise E gleich D, die ist nur eine andere Art, so ein Paar eben zu schreiben.