What does Unification mean?
In computer science and logic, unification is the algorithmic procedure used in solving equations involving symbolic expressions. In other words, by replacing certain sub-expression variables with other expressions, unification tries to identify two symbolic expressions. Unification is used in automated reasoning technology, which remains one of the major application areas of unification.
Unification is used in implementations such as:
Unification is one of the fundamental techniques upon which methods for automated deduction are based.
Unification
The term “unification” and its notion can be attributed to John Alan Robinson. He used unification as the basic operation of his resolution principle and also showed that unifiable terms have at most one general unifier. Several frameworks of unification are differentiated based on the expressions which occur in the unification problem. First order unification is one in which higher order variables (variables representing functions) are permitted in the expressions. Free unification or syntactic unification is one in which a solution is needed in order to make both sides of the equation equal.
The solution of a unification problem is depicted by substitution, which is the mapping of a symbolic value to every variable involved in the problem’s expressions. In other words, The essential focus of unification is to look for a substitution in order to unify two given terms. Higher uniform algorithm is expected to provide a minimal and complete substitution set (a set having all the relevant solutions with no redundant members) for a given problem. In other words, unification is not just interested in solvability of a given unification if problem but also if solvable, in computing the most general unifier.
Unification is considered the core of: