What algorithms for unification over (multidimensional) array terms?
By way of context, I'll assume the goal is to do unification in classical first-order logic in a fixed language $\mathscr{L}$. (Formatting and other corrections welcome.)

Briefly, you can treat arrays as terms and multidimensional arrays as arrays of arrays. You'll also introduce a new term symbol that doesn't occur in $\mathscr{L}$.

So for example, if you have a multidimensional array like the following,

\begin{pmatrix}
1 &amp; 2 &amp; 3\\
x &amp; y &amp; z
\end{pmatrix}

you'll first convert it to an array of arrays,

$$\text{((1 2 3) (x y z))}$$

and then convert it to terms. Assuming the term symbol a is not in your language, you can now represent your multidimensional array as follows:

    a(a(1,2,3),a(x,y,z))