Unification Algorithm
A Calculus 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