A logical calculus for controlled monotonicity