A decision procedure for monotone functions over bounded and complete lattices
Domenico Cantone and Calogero G. Zarba
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 union 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(m^4) for normalized conjunctions of m literals, thus entailing that the quantifier-free satisfiability problem for BLmf is 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.
TARSKI: Theory and Applications of Relational Structures as Knowledge Instruments II, Volume 4342 of LNCS (TARSKI 2006).