We introduce the $k$-variable-occurrence fragment, which is the set of terms having at most $k$ occurrences of variables. We give a sufficient condition for the decidability of the equational theory of the $k$-variable-occurrence fragment using the finiteness of a monoid. As a case study, we prove that for Tarski's calculus of relations with bounded dot-dagger alternation (an analogy of quantifier alternation in first-order logic), the equational theory of the $k$-variable-occurrence fragment is decidable for each $k$.

翻译：我们引入了$k$-变元出现片段，即变元出现次数最多为$k$的项集。我们给出了一个基于幺半群有限性的充分条件，用于判定$k$-变元出现片段的等式理论的可判定性。作为案例研究，我们证明了对于具有有界点-dagger交替（一阶逻辑中量词交替的类比）的塔斯基关系演算，每个$k$对应的$k$-变元出现片段的等式理论都是可判定的。