A Decidable Ground Fragment of the Monotonicity Calculus

Monotonicity is a prevalent feature in natural language. Notably, determiners such as every, some, and no induce monotonic (upward) or antitonic (downward) entailments. The Monotonicity Calculus is a proof system that formalizes such reasoning in natural language inferences through order statements (inequalities) involving higher-order (typed) terms. In this paper, we prove that with a slight modification of the conditions for term formation, it is decidable over ground terms, i.e., terms that contain no variables.