Vorwissen von Unifikation aus "Programmierung"

[tidenhub]

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)

[mkroetzsch]

Danke für diesen Hinweis! Der Unifkationsalgorithmus ist schon seit vielen Jahren Teil der Logikvorlesung (ich habe ihn vor über 15 Jahren bereits selbst in Logik gelernt). Seitdem hat sich aber einiges am Studienaufbau geändert. Da die Ausgestaltung der Lehrveranstaltungen nicht zentral koordiniert wird, werden solche Überlappungen manchmal nicht bemerkt. Bei TheoLog kommt erschwerend dazu, dass die Rotation der Lehre dazu führt, dass es 3-4 unabhängig verwaltete Vorlesungsmaterialien gibt.

Im gegebenen Fall ist vor allem die Überbelegung von Elimination/Eliminierung ungünstig. Da der Stoff in diesem Semester schon schon gelehrt ist, werden wir den Hinweis vor allem bei der Klausurkorrektur berücksichtigen.