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

TL;DR

This paper investigates the decidability of the $k$-variable-occurrence fragment in the calculus of relations, establishing conditions under which its equational theory is decidable, with a focus on Tarski's calculus with bounded dot-dagger alternation.

Contribution

It introduces the $k$-variable-occurrence fragment and proves its decidability for Tarski's calculus of relations with bounded dot-dagger alternation.

Findings

Decidability of the $k$-variable-occurrence fragment's equational theory is established.

A sufficient condition for decidability using monoid finiteness is provided.

The results apply specifically to Tarski's calculus with bounded dot-dagger alternation.

Abstract

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$.