Unification by transformation

Question

I am writing a unification algorithm in F# for use with AST transformations using "Term Rewriting and All That" (WoldCat) by Franz Baader and Tobias Nipkow. For section 4.6 Unification by transformation, it was too much math theory with the examples, and not as clear as I would have liked.

Can someone give or point out simpler examples that make use of transformations:

Delete, Decompose, Orient, Eliminate.

Answer 1

Delete: t = t is pointless and can be removed from the set of equations.

1 =? 1 -> nil

Orient: We want all equations in the form of x =? t, so flip any equations in the form of t =? x.

2 =? x1 -> x1 =? 2

Eliminate: Given x =? t, change all other equations to replace all instances of x with t.

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

Decompose: We need to take any functions and eliminate them to get equations in the form of x =? t. Note that this process technically only removes one function at a time.

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

Hopefully this helps.