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...

Ful tanımlama

Detaylı Bibliyografya
Asıl Yazarlar: Chistikov, D, Haase, C, Mansutti, A
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