The Library
Quantifier elimination for counting extensions of Presburger arithmetic
Tools
Chistikov, Dmitry, Haase, Christoph and Mansutti, Alessio (2022) Quantifier elimination for counting extensions of Presburger arithmetic. In: 25th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2022), Munich, Germany, 2-7 Apr 2022. Published in: Foundations of Software Science and Computation Structures, 13242 pp. 225-243. ISBN 9783030992521. doi:10.1007/978-3-030-99253-8_12 ISSN 0302-9743.
|
PDF
WRAP-quantifier-elimination-counting-extensions-Presburger-arithmetic-oa-Chistikov-2022.pdf - Published Version - Requires a PDF viewer. Available under License Creative Commons Attribution 4.0. Download (494Kb) | Preview |
|
PDF
WRAP-quantifier-elimination-counting-extensions-Presburger-arithmetic-Chistikov-2022.pdf - Accepted Version Embargoed item. Restricted access to Repository staff only - Requires a PDF viewer. Download (637Kb) |
Official URL: https://doi.org/10.1007/978-3-030-99253-8_12
Abstract
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.
Item Type: | Conference Item (Paper) | ||||||||
---|---|---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics | ||||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||||
Library of Congress Subject Headings (LCSH): | Elimination, Numbers, Natural, Arithmetic | ||||||||
Series Name: | Lecture Notes in Computer Science | ||||||||
Journal or Publication Title: | Foundations of Software Science and Computation Structures | ||||||||
Publisher: | Springer | ||||||||
ISBN: | 9783030992521 | ||||||||
ISSN: | 0302-9743 | ||||||||
Official Date: | 2022 | ||||||||
Dates: |
|
||||||||
Volume: | 13242 | ||||||||
Page Range: | pp. 225-243 | ||||||||
DOI: | 10.1007/978-3-030-99253-8_12 | ||||||||
Status: | Peer Reviewed | ||||||||
Publication Status: | Published | ||||||||
Access rights to Published version: | Open Access (Creative Commons) | ||||||||
Date of first compliant deposit: | 1 February 2022 | ||||||||
Date of first compliant Open Access: | 31 March 2022 | ||||||||
RIOXX Funder/Project Grant: |
|
||||||||
Conference Paper Type: | Paper | ||||||||
Title of Event: | 25th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2022) | ||||||||
Type of Event: | Conference | ||||||||
Location of Event: | Munich, Germany | ||||||||
Date(s) of Event: | 2-7 Apr 2022 | ||||||||
Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year