for all $x\in\mathcal{V}$.

\[def:unifprob\]\[def:solprob\] An equation is an unordered pair $t \doteq u$ of terms in $\mathcal{T}_\mathbb{S}$. A unification problem is a set $P=\{t_1 \doteq u_1, ..., t_n \doteq u_n\}$ of equations.

A solution for $P$ is a substitution $\theta$ such that for all equations $t_i \doteq u_i$ in $P$, $\theta t_i = \theta u_i$.

\[def:matching\] Two terms $t$ and $u$ are matchable if there exists a renaming $\alpha$ such that $\{\alpha t \doteq u\}$ has a solution.

\[def:unifalgo\] The problem of deciding if a solution to a given unification problem $P$ exists is decidable. Moreover, there exists a minimal solution $\unifalgo{P}$ w.r.t the preorder $\theta \preceq \psi \Leftrightarrow \exists \theta'.\psi = \theta' \circ \theta$, unique up to renaming.

Let us note that several algorithms were designed to compute the unique solution when it exists, such that the Martelli-Montanari unification algorithm [@martelli1982efficient].

Stars and Constellations {#subsec:stars}
------------------------

The stellar resolution model is based on first-order unification but extends it the notions of *polarities* and *colours*. Intuitively, polarised terms are prefixed with either a $+$ or $-$ sign indicating their ability to be composed (with a term of opposite polarity). Colours allow for the consideration of various types of composition. We 