Monotonicity inference for higher-order formulas


Formulas are often monotonic in the sense that if the formula is satisfiable for given domains of discourse, it is also satisfiable for all larger domains. Monotonicity is undecidable in general, but we devised two calculi that infer it in many cases for higher-order logic. The stronger calculus has been implemented in Isabelle’s model finder Nitpick, where it is used to prune the search space, leading to dramatic speed improvements for formulas involving many atomic types.

In Jürgen Giesl and Reiner Hähnle, editors, Automated Reasoning (IJCAR 2010), volume 6173 of Lecture Notes in Artificial Intelligence, pages 91–106. Springer Verlag, 2010.