Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras

In this paper, we present a resolution-based decision procedure which can be used for deciding unification with linear constant restriction for a large class of finitely-generated varieties of algebras. Since the decidability of V-unification with linear constant restrictions implies the decidability of the positive theory of V, the method presented above yields a decision algorithm for the positive theory of V. The method is based on the existence of natural duality theorems for such classes of algebras.