Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators

We establish a link between the satisfiability of universal sentences with respect to classes of distributive lattices with operators and their satisfiability with respect to certain classes of relational structures. This justifies a method for structure-preserving translation to clause form of universal sentences in such classes of algebras. We show that refinements of resolution yield decision procedures for the universal theory of some such classes. In particular, we obtain exponential space and time decision procedures for the universal clause theory of (i) the class of all bounded distributive lattices with operators satisfying a set of (generalized) residuation conditions, and (ii) the class of all bounded distributive lattices with operators, and a doubly-exponential time decision procedure for the universal clause theory of the class of all Heyting algebras.