A Decision Procedure for Monotone Functions over Lattices.
Domenico Aldo Cantone, Calogero G. Zarba · APPIA-GULP-PRODE · 2003
This paper presents a practical decision procedure for the unquantified theory of lattices with monotone functions. Specifically, it considers the unquantified language Lmf with the predicates = and ≤ and with the operators inf and sup over terms which may involve also uninterpreted function symbols. Additional predicates expressing increasing and decreasing monotonicity of functions are allowed as well as a predicate for pointwise functions comparison. For a restricted collection of conjunctions, denoted Lmf, we give a quadratic satisfiability test. We also describe a nondeterministic quadratic reduction of the satisfiability problem for Lmf -formulae to the one for Lmf, which allows to prove the NP-completeness of the former problem.