Los puntos clave no están disponibles para este artículo en este momento.
We consider the fragment of Second-Order unification with the following properties: (i) only one second-order variable allowed, (ii) first-order variables do not occur. We show that Hilbert's 10^th problem is reducible to this fragment if the signature contains a binary function symbol and two constants. This generalizes known undecidability results. Furthermore, We show that adding the following restriction: (i) the second-order variable has arity 1, (ii) the signature is finite, and (iii) the problem has bounded congruence, results in a decidable fragment. The latter fragment is related to Bounded second-order unification, i. e. the number of holes is a function of the problem structure.
Cerna et al. (Tue,) studied this question.