Decidability of $\Delta$-equivalence problem for monadic logic programs

In the present paper the $\Delta$-equivalence problem of monadic logic programs (logic programs using only monadic functional and predicate symbols) is investigated. It is shown that contrary to the general case, the relation of $\Delta$-equivalence is decidable in case of monadic programs. Our proof is based on the decidability of Rabin’s monadic second order logic of successor functions.