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 ...

Start Free Trial

No credit card required