We present a generalization of first-order unification to a term algebra where variable indexing is part of the object language. We exploit variable indexing by associating some sequences of variables ($X_0,\ X_1,\ X_2,\dots$) with a mapping $\sigma$ whose domain is the variable sequence and whose range consist of terms that may contain variables from the sequence. From a given term $t$, an infinite sequence of terms may be produced by iterative application of $\sigma$. Given a unification problem $U$ and mapping $\sigma$, the \textit{schematic unification problem} asks whether all unification problems $U$, $\sigma(U)$, $\sigma(\sigma(U))$, $\dots$ are unifiable. We provide a terminating and sound algorithm. Our algorithm is \textit{complete} if we further restrict ourselves to so-called $\infty$-stable problems. We conjecture that this additional requirement is unnecessary for completeness. Schematic unification is related to methods of inductive proof transformation by resolution and inductive reasoning.

翻译：我们提出一种将一阶统一化推广至项代数的方法，其中变量索引作为对象语言的一部分。通过将某些变量序列（$X_0,\ X_1,\ X_2,\dots$）与一个定义域为该变量序列、值域为可包含序列中变量的项集合的映射 $\sigma$ 相关联，我们利用变量索引进行运算。从给定项 $t$ 出发，通过迭代应用 $\sigma$，可生成无限项序列。给定统一化问题 $U$ 与映射 $\sigma$，_模式统一化问题_探究是否所有统一化问题 $U$、$\sigma(U)$、$\sigma(\sigma(U))$、……均可统一化。我们提供了一种可终止且可靠的算法。若进一步限制于所谓的 $\infty$-稳定问题，则该算法是_完备的_。我们推测该额外限制对于完备性并非必要。模式统一化与基于消解和归纳推理的归纳证明变换方法相关。