We present a decision procedure for the quantifier-free satisfiability problem of the language
BLmf of bounded lattices with monotone unary functions. The language contains the predicates = and ≤, as well as the operators⊓and
⊔ over terms which may involve uninterpreted unary function symbols. The language also contains predicates for expressing
increasing and decreasing monotonicity of functions, as well as a predicate for pointwise function comparison.
Our decision procedure runs in polynomial time
O(m4){\mathcal{O}(m^{4})} for normalized conjunctions of
m literals, thus entailing that the quantifier-free satisfiability problem for
BLmf is
NP\mathcal{NP}-complete. Furthermore, our decision procedure can be used to decide the quantifier-free satisfiability problem for the language
CLmf of complete lattices with monotone functions. This allows us to conclude that the languages
BLmf and
CLmf are equivalent for quantifier-free formulae.