Why is unification so important to inference engines?

Problem Detail: 

^{I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here.}

I keep reading about the Unification Algorithm.

• What is it and why is so important to Inference Engines?
• Why is it so important to Computer Science?

Asked By : Guy Coder

Answered By : Dave Clarke

Unification is such a fundamental concept in computer science that perhaps at time we even take it for granted. Any time we have a rule or equation or pattern and want to apply it to some data, unification is used to specialize the rule to the data. Or if we want to combine two general but overlapping rules, unification provides us with the most general combined rule. Unification is at the core of

• Theorem provers and proof assistants, include some based on higher-order unification.
• Prolog implementations (as Resolution).
• Type inference algorithms.
• Computational linguistics/natural language processing.
• Term rewriting systems such as Maude, which can be used as the basis of programming language semantics.
• Deductive databases.
• Expert systems or more generally Artificial intelligence.
• Computer algebra systems.
• Pattern matching in functional languages (at least in part ... only matching).
• Some parsing approaches.
• Some query languages, especially involving the Semantic Web.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/882