Quantifier elimination for counting extensions of Presburger arithmetic
We give a new quantifier elimination procedure for Presburger arithmetic extended with a unary counting quantifier ∃=xyΦ that binds to the variable x the number of different y satisfying Φ. While our procedure runs in non-elementary time in general, we show that it yields nearly optimal elementary c...
| Những tác giả chính: | , , |
|---|---|
| Định dạng: | Conference item |
| Ngôn ngữ: | English |
| Được phát hành: |
Springer
2022
|