On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation

07/11/2023
by   Yoshiki Nakamura, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset