An efficient quantifier elimination procedure for Presburger arithmetic

Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani +2

All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has e…