非表示:
キーワード:
-
要旨:
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,
(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.
