Presburger arithmetic with threshold counting quantifiers is easy
share
We give a quantifier elimination procedures for the extension of Presburger arithmetic with a unary threshold counting quantifier ∃^≥ c y that determines whether the number of different y satisfying some formula is at least c ∈ℕ, where c is given in binary. Using a standard quantifier elimination procedure for Presburger arithmetic, the resulting theory is easily seen to be decidable in 4ExpTime. Our main contribution is to develop a novel quantifier-elimination procedure for a more general counting quantifier that decides this theory in 3ExpTime, meaning that it is no harder to decide than standard Presburger arithmetic. As a side result, we obtain an improved quantifier elimination procedure for Presburger arithmetic with counting quantifiers as studied by Schweikardt [ACM Trans. Comput. Log., 6(3), pp. 634-671, 2005], and a 3ExpTime quantifier-elimination procedure for Presburger arithmetic extended with a generalised modulo counting quantifier.
READ FULL TEXT