Unification Algorithm

A Calculus $\mathcal{U}$ to solve the Unification Problem with the following rules:

Decomposition Rule, Trivial Rule, Elimination Rule.

Elimination Rule is kind of like Constraint Propagation.

This algorithm is

• correct
• complete
• correct + complete → the MGU of all derived forms (including the Solved Form) is the same as the problem in the beginning
• Confluent
  • there can only be one MGU

→ this is unitary, so MGUs are unique

We are doing tightenens that are equivalent.

Correctness and Completeness ←→ Tightness and Equivalence in CSP