On the universal theory of varieties of distributive lattices with operators: some decidability and complexity results

摘要

In this paper we establish a link between satisfiability of universal sentences with respect to varieties of distributive lattices with operators and satisfiability with respect to certain classes of relational structures. we use these results for giving a method for translation to clause form of universal sentences in such varieties, and then use results from automated theorem proving to obtain decidability and complexity results for the universal theory of some such varieties.