On Unication for Bounded Distributive Lattices
Viorica Sofronie-Stokkermans · 2000
We give a resolution-based procedure for deciding uniability in the variety of bounded distributive lattices. The main idea is to use a structure-preserving translation to clause form to reduce the problem of testing the satisability of a unication problem S to the problem of checking the satisability of a set S of (constrained) clauses. These ideas can be used for unication with free constants and for unication with linear constant restrictions. Complexity issues are also addressed.