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.#R##N##R##N#Our decision procedure runs in polynomial time ${\mathcal{O}(m^{4})}$ for normalized conjunctions of m literals, thus entailing that the quantifier-free satisfiability problem for BLmf is $\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.
['Domenico Cantone', 'Calogero G. Zarba']
A decision procedure for monotone functions over bounded and complete lattices