Unifikation < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 16:31 Mo 22.02.2016 | | Autor: | Mime |
| Aufgabe | Entscheiden Sie, ob folgende Termfolge unifizierbar ist. Geben Sie gegebenfalls eine universelle Termfolge und das Resultat der Unifizierung an.
[mm] S^1 [/mm] = (x, h(a, z), f(x))
[mm] S^2 [/mm] = (g(g(v)), y, f(w)) |
Hallo liebes Forum :)
An sich ist mir klar, wie die Unifizierung funktioniert, es stellen sich mir jedoch kleinere Fragen, die während der Unifizierung auftreten:
[mm] S^1 [/mm] = (x, h(a, z), f(x))
= [mm] S^1 [/mm] (x, z, v, y, w)
Gibt es hier eine bestimmte Reihenfolge für die einzelnen Teile, damit die Reihenfolge am Schluss mit der Reihenfolge des Resultats der Unifizierung übereinstimmt?
[mm] S^2 [/mm] = (g(g(v)), y, f(w))
= [mm] S^2 [/mm] (x, z, v, y, w)
Gleiche Frage wie oben drüber.
Die Termfolge ist unifizierbar wenn
[mm] S^1 (t_1, [/mm] . . . [mm] ,t_n) [/mm] = [mm] S^2 (t_1, [/mm] . . . [mm] ,t_n)
[/mm]
Nun ist:
S = {x = g(g(v)), h(a, z) = y, f(x) = f(w)}
Schritt A:
Ersetze f(x) = f(w) durch x = w.
Schritt B:
Ersetze x durch g(g(v)), y durch h(a, z)
=> w = g(g(v)).
T = (g(g(v)), z, v, h(a,z), g(g(v)))
(Ist dies die "universelle unifizierende Termfolge"?)
[mm] S^1 [/mm] (g(g(v)), z, v, h(a,z), g(g(v))) = (g(g(v)), h(a,z), f(g(g(v))))
= [mm] S^2 [/mm] (g(g(v)), z, v, h(a,z), g(g(v)))
Ist der unterstrichende Teil das "Resultat der Unifizierung"? Des Weiteren verstehe ich nicht warum da f(g(g(v))) stehen muss und nicht nur g(g(v))?
Ich hoffe jemand kann mir diese Unklarheiten erklären.
Viele Grüße,
Mime
Ich habe diese Frage in keinem Forum auf anderen Internetseiten gestellt.
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 17:20 Di 01.03.2016 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
