Vorwissen von Unifikation aus "Programmierung"

Das Thema Unifikation wurde schon in der Vorlesung "Programmierung" von Prof. Dr. Vogler behandelt. Ich bin der Meinung, dass es in der TheoLog Vorlesung gut etwas kürzer gefasst werden könnte.

Ich würde es für sinnvoll halten, wenn man sich bei der Benennung der Regel für den Unifikationsalgorithmus absprechen könnte. Gerade die Regel "Eliminierung" kann leicht verwechselt werden:

* *TheoLog = Programmierung*
* Löschen = Elimination
* Zerlegung = Dekomposition
* Orientierung = Vertauschung
* Eliminierung = Substitution

Auch bei der Notation wäre eine Vereinheitlichung wünschenswert.

Gerne würde ich an dieser Stelle den Auszug aus dem Skript verlinken, dass aber nur in gedruckter Form vorliegt. Stattdessen kann ich nur auf eine Hilfsfolie aus der Übung verlinken:
https://drive.google.com/file/d/0B-hi46IhP-LNQUhFRlNkMkd2LTQ/view?usp=sharing (Ab Seite 4)