Unification

Consider expressions built up from variables and constants using function symbols. If , ...,  are variables and , ...,  are expressions, then a set of mappings between variables and expressions {t_1|v_1,...,t_n|v_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline5.svg" style="height:24px; width:140px" /> is called a substitution.

If {t_1|v_1,...,t_n|v_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline6.svg" style="height:24px; width:173px" /> and  is an expression, then  is called an instance of  if it is received from  by simultaneously replacing all occurrences of  (for ) by the respective .

If {t_1|v_1,...,t_n|v_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline14.svg" style="height:24px; width:173px" /> and {u_1|x_1,...,u_n|x_m}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline15.svg" style="height:24px; width:185px" /> are two substitutions, then the composition of  and  (denoted ) is obtained from {t_1theta|v_1,...,t_ntheta|v_n,u_1|x_1,...,u_n|x_m}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline19.svg" style="height:24px; width:314px" /> by removing all elements  such that  and all elements  such that  is one of , ..., .

A substitution  is called a unifier for the set of expressions {E_1,...,E_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline27.svg" style="height:22px; width:92px" /> if . A unifier  for the set of expressions {E_1,...,E_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline30.svg" style="height:22px; width:92px" /> is called the most general unifier if, for any other unifier for the same set of expressions , there is yet another unifier  such that .

A unification algorithm takes a set of expressions as its input. If this set is not unifiable, the algorithm terminates and yields a negative result. If there exists a unifier for the input set of expressions, the algorithm yields the most general unifier for this set of expressions. The unification algorithm serves as a tool for the resolution principle. It is also a basis for term rewriting systems.

---

REFERENCES

Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.

مواضيع ذات صلة

Lemma

Proof

Zeno,s Paradoxes

Unexpected Hanging Paradox

Strange Loop

Sorites Paradox

Simpson,s Paradox

Russell,s Antinomy

Paradox

Newcomb,s Paradox

Missing Dollar Paradox

Line Point Picking