Monotonicity inference for higher-order formulas (Q438558)

The authors investigate possibilities of inferring monotonicity of formulae for higher-order logic. This is mainly motivated by their work on model finding, where monotonicity can help prune search space; it is mentioned that another use of monotonicity is to find finite substructures of infinite models. A formula \(t\) in higher-order logic is monotonic w.r.t.\ a type variable \(\alpha\) if for all scopes \(S\), \(S'\) such that \(S \leq_{\alpha} S'\), if \(t\) is satisfiable for \(S\) then it is also satisfiable for \(S'\). The formula \(t\) is antimonotonic w.r.t. \(\alpha\) if its negation is monotonic w.r.t. \(\alpha\). It is first shown that monotonicity w.r.t.\ \(\alpha\) is undecidable. Then three calculi for inferring monotonicity are presented. The first calculus is based on tracking equality and quantifiers. The second calculus -- based on tracking sets -- addresses some of the problems the first calculus has. The drawback of this second calculus is that it cannot type set comprehension precisely (as a result it cannot infer, for instance, monotonicity of any of the four type-variables occurring in the associativity law for composition). These problems are addressed in a third calculus which handles set comprehension and bounded quantifications. The implementation of these calculi in \texttt{Isabelle}'s model finder \texttt{Nitpick} is evaluated on the user-supplied theorems from six highly polymorphic \texttt{Isabelle} theories. The tests show that especially the use of the third calculus leads to considerable speed and precision improvements.