Presburger arithmetic with threshold counting quantifiers is easy

Dmitry Chistikov, Christoph Haase, Alessio Mansutti

We give a quantifier elimination procedures for the extension of Presburger arithmetic with a unary threshold counting quantifier ${\exists }^{\ge c}y$ that determines whether the nu…