I have formulas in Presburger arithmetic (with initial , but I can apply quantifier elimination so they are quantifier-free) that are fairly complicated, yet, in many useful cases, are equivalent to very simple formulas such as conjunctions of simple arithmetic constrains (e.g. p>=-1, p<q, y>=q, y<n, n>=2 for a quantified formula taking up a whole screen page).Is there any good simplification method for such formulas? (preferably in an off-the-shelf implementation)
Simplification of Presburger formulas in practice
lo.logic