A Decision Procedure for Monotone Functions over Bounded and Complete Lattices

摘要

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(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.