Handbook of Automated Reasoning

3.3.3 The category-theoretic point of view

Let $\Gamma :=\left\{s_i{=}_E^{?}{t}_i\right|i=1,\dots ,n\}$ be an E-unification problem over $\mathcal{F}$ , and $\mathcal{X}:=\mathcal{V}ar\left(\Gamma \right)$ be the finite set of variables occurring in Γ. Since all our calculations are done modulo E, we may consider the terms s _i and t _i as elements of $\mathcal{T}\left(\mathcal{F},\mathcal{X}\right)/{=}_E$ , the .E-free algebra with generators $\mathcal{X}$ . For example, let $\mathcal{F}$ consist of a binary ...