论带有点-匕首有界交替的关系演算的有限变量出现片段
On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation
AI总结：
本文引入 $k$-变量出现片段，利用幺半群有限性给出等式理论可判定的充分条件，并证明带点-匕首有界交替的 Tarski 关系演算在该片段下对每个 $k$ 均可判定。
摘要：
我们引入了 $k$-变量出现片段，即最多包含 $k$ 次变量出现的项的集合。我们利用幺半群的有限性，给出了 $k$-变量出现片段等式理论可判定的一个充分条件。作为案例研究，我们证明了对于带有点-匕首有界交替（类似于一阶逻辑中量词交替）的 Tarski 关系演算，$k$-变量出现片段的等式理论对每个 $k$ 都是可判定的。
英文摘要：
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$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
