How is term rewriting different from unification, and what's the difference between term rewriting languages and logic programming, like Prolog?
Term Rewriting vs Unification
terminology;term rewriting;logic programming;unification
Term rewriting is a rewriting formalism. Starting with a term we rewrite the term according to the term rewriting rules until a normal form is found. Unification is finding a solution (substitution with specific properties) to a problem (a pair of terms).Term rewriting uses a notion called pattern matching. What you probably meant is: what is the difference between matching and unification?Let two terms $t_1$ and $t_2$ be given.If we want to unify $t_1$ and $t_2$, we search for a substitution $\sigma$ such that $t_1\sigma = t_2\sigma$. On the other hand, if we want to match $t_1$ into $t_2$, we are looking for a substitution such that $t_1\sigma = t_2$. That is, we apply the substitution only on $t_1$.Logic programming is a programming paradigm which is based on resolution, which is a proof method for logics. In logic programming unification plays an important role.