Wir wollten heute oder ich möchte gerne heute die Logik erster Stufe abschließen, damit wir

vor dem Ende des Semesters noch ein Kapitel über Planung durchkriegen. Wir waren als Großthema bei

automatischen, also bei maschinenorientierten Kalkülen für die Logik erster Stufe und hatten

uns erstmal den Tableau Kalkül angeguckt und hatten dafür neue Quantorenregeln und

eine neue Schnittregel eingeführt. Und die Kernidee hierbei war, dass man das Raten von

Instanzen, wenn wir ein Alquanto haben, müssen wir irgendeine Instanz dafür finden. Und das

kann irgendein Term sein und davon gibt es im Unmöglich viele, dass wir das möglichst weit

verzögern. Das geht auch, indem wir einfach Variablen einsetzen und hoffen, dass sie später

immer weiter instanziert werden, bis es alles einfacher ist. Das hat aber zwei Preise, die man

bezahlen muss. Das eine ist, man muss skolemisieren, man muss diese Skolem-Funktionen hier einsetzen,

angewandt auf freie Variablen, in das wiederum dann Krempel eingesetzt wird, um die Abhängigkeiten

zwischen allquantifizierten und existenzquantifizierten Variablen im Blick zu behalten. Und das Zweite ist,

dass wir die Schnittregel für allgemeineren Munten, dass man zwischen beliebigen Literalen

schneiden kann, wenn man sie denn gleich machen kann. Und das hat diese Operation der Unifikation

motiviert, die wir dann im nächsten uns genau angeguckt haben. Das erste, was wir uns angeguckt

haben, war, dass es da auch sehr viele gibt, aber dass man sie alle repräsentieren kann durch den

sogenannten allgemeinsten Unifikator, also denjenigen Unifikator, den man zu jedem anderen

weiter instanzieren kann. Das ist sozusagen die Substitution, die zwei Terme gleich macht,

aber sich am allerwenigsten festlegt. Und das ist genau das, was wir natürlich in dieser

Schnittregel haben wollen. Wir möchten uns möglichst wenig festlegen, damit wir hinterher noch

weitermachen können durch Instanzierung. Diese allgemeinsten Unifikatoren will man finden. Man

hat also minimale Elemente, allgemeinste Elemente, die die anderen alle repräsentieren. Und die Frage

ist, kann ich die berechnen? Und die Idee hinter dem Unifikationsalgorithmus, den wir uns

angeguckt haben, war, dass wir ihn als ein Transformationssystem aufschreiben. Dass wir sagen,

wir haben Repräsentationen des Problems, Gleichungssysteme. Und diese Gleichungssysteme

formen wir so lange um, bis die Lösung ablesbar ist. Das heißt, wir definieren erst mal ein

Gleichungssystem und den schreiben wir so als eine artlogische Formel, wo man im Kopf behält,

dass und-kommutativ und assoziativ und idempotent ist. Also das heißt im Wesentlichen, ich darf die

uns umsortieren, wie ich will. Ich kann sie ohne Klammern schreiben und wenn ich doppelte Elemente

habe, kann ich die zusammenfassen. Und außerdem, dass die Gleichheiten hier drin, dass ich die umdrehen

darf, so wie ich möchte. Andere Leute schreiben, dass mit Mengen von Zweiermengen oder von Paaren

oder irgendwie sowas, ich finde diese schreibweise hübsch, egal wie man es macht, man hat irgendwie

Mengen von Gleichungen und Gleichungen darf man umdrehen. Wir definieren eine gelöste Form,

gelöste Form, eine Form aus der man die Lösung gleich ablesen kann und überzeugen uns davon,

dass die Lösung, die man abliest, das ist sehr wichtig, auch tatsächlich der allgemeinste Unifikator

dieser gelösten Form ist. Wie machen wir das? Wir erinnern uns daran, dass ein Unifikator

allgemeiner ist als ein anderer, wenn ich ihn, wenn ich den weniger Allgemeinen bekommen kann,

dadurch, dass ich den Allgemeineren weiter instanziere, indem ich eine weitere Substitution

davor schalte, dass es in diesem Fall hier dieses, wir wollen zeigen, das TETA ist irgendwie irgendeine

Substitution, ich sollte dahin funzeln, so war das, ist irgendeine Substitution hinterher

geschaltet, hinter das Sigma E und diese Substitution, die wir finden wollten, in diesem Fall ist TETA

wieder selber. Das heißt, wir haben einen allgemeinsten Unifikator. Und dann können wir das

Transformationssystem relativ einfach concerning aufschreiben. Wir haben drei Regeln, die einfachste ist

die Trivialitätsregel, wo wir gleiche Paare einfach wegschmeißen können. Dann haben wir die

Decompositionsregel, indem wir今日は zwei Therm거hen die die gleichen Kopfsymbole haben.

Dann kann man einfach die Argumente vergleichen und wir haben die evolvedens velbale

Eliminationsregel, dass wenn ich ein Paar habe, was schon so ein bisschen gelöst aussieht,

Variable gleich Termen, wo ich dann eine Substitution a für x auf den Rest des Problems anwende.

Zwei Dinge, die da drin zu beachten sind, ist einmal diese, wir dürfen nicht zulassen,

dass x in den freien Variablen von a vorkommt, denn solche Paare sind unlösbar, davon hatten