Simple and Minimal Ground Term Equation Systems

Abstract

A ground term equation system (gtes for short) E is simple if there is no gtes E′ equivalent to E consisting of less equations than E has. Moreover, a gtes E is minimal if for each equation e ∈ E, the congruence generated by E – {e} is a proper subset of the congruence generated by E. Given a reduced ground term rewriting system R, we describe all simple gtes' E and minimal gtes' F equivalent to R. We show that for a reduced ground term rewriting system R, it is decidable whether or not there exist infinitely many simple (minimal) gtes' equivalent to R. Finally, we show that for a reduced ground term rewriting system R, and a gtes E, it is decidable if there is a simple gtes F equivalent to R such that E ⊆ F.