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...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2022
|
| _version_ | 1826307533139083264 |
|---|---|
| author | Chistikov, D Haase, C Mansutti, A |
| author_facet | Chistikov, D Haase, C Mansutti, A |
| author_sort | Chistikov, D |
| collection | OXFORD |
| description | 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 complexity results for expressive counting extensions of Presburger arithmetic, such as the threshold counting quantifier ∃≥cyΦ that requires that the number of different y satisfying Φ be at least c∈N, where c can succinctly be defined by a Presburger formula. Our results are cast in terms of what we call the monadically-guarded fragment of Presburger arithmetic with unary counting quantifiers, for which we develop a 2EXPSPACE decision procedure. |
| first_indexed | 2024-03-07T07:04:32Z |
| format | Conference item |
| id | oxford-uuid:4543c7fa-61ce-4e09-8362-6ddb953d2a1f |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:04:32Z |
| publishDate | 2022 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:4543c7fa-61ce-4e09-8362-6ddb953d2a1f2022-04-28T10:03:32ZQuantifier elimination for counting extensions of Presburger arithmeticConference itemhttp://purl.org/coar/resource_type/c_5794uuid:4543c7fa-61ce-4e09-8362-6ddb953d2a1fEnglishSymplectic ElementsSpringer2022Chistikov, DHaase, CMansutti, AWe 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 complexity results for expressive counting extensions of Presburger arithmetic, such as the threshold counting quantifier ∃≥cyΦ that requires that the number of different y satisfying Φ be at least c∈N, where c can succinctly be defined by a Presburger formula. Our results are cast in terms of what we call the monadically-guarded fragment of Presburger arithmetic with unary counting quantifiers, for which we develop a 2EXPSPACE decision procedure. |
| spellingShingle | Chistikov, D Haase, C Mansutti, A Quantifier elimination for counting extensions of Presburger arithmetic |
| title | Quantifier elimination for counting extensions of Presburger arithmetic |
| title_full | Quantifier elimination for counting extensions of Presburger arithmetic |
| title_fullStr | Quantifier elimination for counting extensions of Presburger arithmetic |
| title_full_unstemmed | Quantifier elimination for counting extensions of Presburger arithmetic |
| title_short | Quantifier elimination for counting extensions of Presburger arithmetic |
| title_sort | quantifier elimination for counting extensions of presburger arithmetic |
| work_keys_str_mv | AT chistikovd quantifiereliminationforcountingextensionsofpresburgerarithmetic AT haasec quantifiereliminationforcountingextensionsofpresburgerarithmetic AT mansuttia quantifiereliminationforcountingextensionsofpresburgerarithmetic |