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...
Asıl Yazarlar: | , , |
---|---|
Materyal Türü: | Conference item |
Dil: | English |
Baskı/Yayın Bilgisi: |
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 |