Sciweavers

CADE
2010
Springer

Monotonicity Inference for Higher-Order Formulas

13 years 4 months ago
Monotonicity Inference for Higher-Order Formulas
Abstract. 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.
Jasmin Christian Blanchette, Alexander Krauss
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CADE
Authors Jasmin Christian Blanchette, Alexander Krauss
Comments (0)