How to solve an unification problem on $\mathbb{N}$? Usually, the unification problem for two given terms $t$ and $s$ is to find a substitution $\theta$ such that $\theta t = \theta s$,
which is equal to finding the certain $\langle x_1 , \cdots , x_n \rangle$ such that $t = s$ holds.
But in the $\lambda$Prolog programming language, by the existence of the logical operator $\mathtt{pi}$ whose semantics resembles $\forall$, an unification problem is of the form
$$ \mathcal{Q}_1 x_1 \cdots \mathcal{Q}_n x_n \left[ t_1 = s_1 \land \cdots \land t_m = s_m \right] , $$
where $\mathcal{Q}_i$ is an universal or existential quantifier.
See Miller's paper for more details.
I made my own $\lambda$Prolog interpreter without the operator of $+$ and $\times$, in which the currently implemented are numerals and successor.
Now, what I want to do is to add both $+$ and $\times$ with their arithmetic semantics, i.e., I want to solve the decision problem:
$$ \mathbb{N} \models \mathcal{Q}_1 x_1 \cdots \mathcal{Q}_n x_n \left[ t_1 = s_1 \land \cdots \land t_m = s_m \right] , $$
where $\mathcal{Q}_i$ is a quantifier, $x_i$ is a variable, $t_j$ and $s_j$ are terms; and terms are $\lambda$-terms extended with the constants $0$, $S$, $+$ and $\times$.
I have concluded that one cannot add both + and × in the λProlog programming language with their arithmetic semantics since the decision problem is undeciable. Because if it was decidable then Hilbert's tenth problem would have a positive answer. See the Wikipedia page for Hilbert's tenth problem.