The process by which one can make different logical expressions identical is the ‘Unification’ process.
In this process, lifted inferences need to find substitute which can make a different expression looks a like.
According to computer science and logic, unification is an algorithm which is used in solving equations and involves symbolic expressions. To be clearer in my words, unification tries to identify two symbolic expressions by replacing certain sub-expression variables with other expressions. One of the major application areas of unification is in automated reasoning technology.
Unification is used in implementations such as:
• Programming language-type system implementation
• Logic programming
• SMT solvers
• Cryptographic protocol analysis
• Term-rewriting algorithms
One of the most fundamental techniques upon which methods for automated deduction are based is the ‘Unification’.
this gives you a basic idea of unification process!!!