An efficient and unified approach to the decidability of equivalence of propositional programs

Abstract

The aim of this paper is to present a unified and easy-to-use technique for deciding the equivalence problem for propositional deterministic programs. The key idea is to reduce this problem to the wellknown group-theoretic problems by revealing an algebraic nature of program computations. By applying the main theorems of this paper to some traditional computational models we demonstrate that the equivalence problem for these models is decidable by the simple algorithms in polynomial time.