Unification (computer Science)
Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact either identical or just equal. Unification is widely used in automated reasoning, logic programming and programming language type system implementation.
Several kinds of unification are commonly studied: that for theories without any equations (the empty theory) is referred to as syntactic unification: one wishes to show that (pairs of) terms are identical. If one has a non-empty equational theory, then one is typically interested in showing the equality of (a pair of) terms; this is referred to as semantic unification. Since substitutions can be ordered into a partial order, unification can be understood as the procedure of finding a join on a lattice.
Unification on ground terms is just the ground word problem; because the ground word problem is undecidable, so is unification.
The first formal investigation of unification can be attributed to John Alan Robinson, who used first-order unification as a basic building block of his resolution procedure for first-order logic, a great step forward in automated reasoning technology, as it eliminated one source of combinatorial explosion: searching for instantiation of terms.
Read more about Unification (computer Science): Informal Overview, Definition of Unification For First-order Logic, Unification in Logic Programming, Type Inference, Higher-order Unification, Examples of Syntactic Unification of First-order Terms, A Unification Algorithm