Vereinigung durch Transformation

Question

Ich schreibe eine Vereinigung algorithmus in F # zur Verwendung mit AST transformationen mit "Umschreiben von Begriffen und all das" (Weltkatze) von Franz Baader und Tobias Nipkow.Für Abschnitt 4.6 Vereinheitlichung durch Transformation war es zu viel mathematische Theorie mit den Beispielen und nicht so klar, wie ich es mir gewünscht hätte.

Kann jemand einfachere Beispiele nennen oder aufzeigen, die Transformationen nutzen:

Löschen, Zerlegen, Orientieren, Eliminieren.

Answer 1

Löschen: t = t ist sinnlos und kann aus dem Gleichungssatz entfernt werden.

1 =? 1 -> nil

Orientieren:Wir wollen alle Gleichungen in Form von x =? t, also Flip irgendwelche Gleichungen in Form von t =? x.

2 =? x1 -> x1 =? 2

Beseitigen:Gegeben x =? t, ändere alle anderen Gleichungen, um alle Instanzen von zu ersetzen x mit t.

x1 + x2 = 7, x2 = 5 -> x1 + 5 = 7, x2 = 5

Zersetzen:Wir müssen irgendwelche Funktionen nehmen und sie eliminieren, um Gleichungen in Form von zu erhalten x =? t.Beachten Sie, dass bei diesem Vorgang technisch jeweils nur eine Funktion entfernt wird.

x1 + 5 = 7 -> x1 = 2
2 * (x1 + x2) = 14 -> x1 + x2 = 7

Hoffentlich hilft das.