非表示:
キーワード:
-
要旨:
We give a method for deciding unifiability in the variety
of bounded distributive lattices.
For this, we reduce the problem of deciding whether a
unification problem ${\cal S}$ has a solution to the
problem of checking the satisfiability of a set
$\Phi_{\cal S}$ of ground clauses.
This is achieved by using a structure-preserving
translation to clause form.
The satisfiability check can then be performed
either by a resolution-based theorem prover or
by a SAT checker. We apply the method to
unification with free constants and to unification
with linear constant restrictions, and show that,
in fact, it yields a decision procedure for the positive
theory of the variety of bounded distributive lattices.
We also consider the problem of unification over
(i.e.\ in an algebraic extension of) the free lattice.
Complexity issues are also addressed.
