Undecidability of the Positive Calculus of Relations with Transitive Closure and Difference: Hypothesis Elimination Using Graph Loops

We show that the equational theory is undecidable and \(\mathrm {\Pi }^{0}_{1}\) -complete for the positive calculus of relations with transitive closure and the difference constant. Furthermore, we show that the emptiness (unsatisfiability) problem is also \(\mathrm {\Pi }^{0}_{1}\) -complete for propositional while-programs with graph loops on functional structures. To this end, we give a hypothesis elimination using graph loops. Using this, we give reductions from the periodic domino problem.