Editing Presburger arithmetic (section)

==Bibliography==
{{Refbegin}}

*{{cite journal
 |last= Berman
 |first= L.
 |year= 1980
 |title= The Complexity of Logical Theories
 |journal= [[Theoretical Computer Science (journal)|Theoretical Computer Science]]
 |volume= 11
 |issue= 1
 |pages= 71–77
 |doi= 10.1016/0304-3975(80)90037-7
 |doi-access= free
}}

*{{cite conference
 |last= Büchi
 |first= J. Richard
 |author-link= Julius Richard Büchi
 |year= 1962
 |title= On a Decision Method in Restricted Second Order Arithmetic
 |conference= Proceedings of the International Congress for Logic
 |book-title= Logic, methodology and philosophy of science
 |location= Stanford
 |pages= 1–11
 |publisher= [[Stanford University Press]]
 |editor1-last= Nagel
 |editor1-first= Ernest
 |editor1-link= Ernest Nagel
 |editor2-last= Suppes
 |editor2-first= Patrick
 |editor2-link= Patrick Suppes
 |editor3-last= Tarski
 |editor3-first= Alfred
 |editor3-link= Alfred Tarski
}}

*{{cite journal
 |last= Cobham
 |first= Alan
 |author-link= Alan Cobham (mathematician)
 |year= 1969
 |title= On the base-dependence of sets of numbers recognizable by finite automata
 |journal= Math. Systems Theory
 |volume= 3
 |issue= 2
 |pages= 186–192
 |doi=10.1007/BF01746527
 |s2cid=19792434
}}

*{{Cite journal
 |last= Cooper
 |first= D.C.
 |year= 1972
 |title= Theorem Proving in Arithmetic without Multiplication
 |journal= Machine Intelligence
 |volume= 7
 |editor1-last= Meltzer
 |editor1-first= B.
 |editor2-last= Michie
 |editor2-first= D.
 |publisher= [[Edinburgh University Press]]
 |pages= 91–99
 |url= https://www21.in.tum.de/teaching/logik/SS16/Exercises/Cooper.pdf
}}

*{{cite journal
 |last1= Eisenbrand
 |first1= Friedrich
 |authorlink1=Friedrich Eisenbrand
 |last2= Shmonin
 |first2= Gennady
 |year= 2008
 |title= Parametric Integer Programming in Fixed Dimension
 |journal= [[Mathematics of Operations Research]]
 |volume= 33
 |issue= 4
 |pages= 839–850
 |arxiv= 0801.4336
 |doi= 10.1287/moor.1080.0320 
|s2cid= 15698556
 }}

*{{Cite book
 |last= Enderton
 |first= Herbert
 |year= 2001
 |title= A mathematical introduction to logic
 |publisher= [[Academic Press]]
 |location= Boston, MA
 |edition= 2nd
 |isbn= 978-0-12-238452-3
}}

*{{cite book
 |last1= Ferrante
 |first1= Jeanne
 |author-link1= Jeanne Ferrante
 |last2= Rackoff
 |first2= Charles W.
 |year= 1979
 |title= The Computational Complexity of Logical Theories
 |series= Lecture Notes in Mathematics
 |volume= 718
 |publisher= [[Springer-Verlag]]
 |doi= 10.1007/BFb0062837
 |isbn= 978-3-540-09501-9
 |mr= 0537764
}}

*{{cite conference
 |last1= Fischer
 |first1= Michael J.
 |author-link1= Michael J. Fischer
 |last2= Rabin
 |first2= Michael O.
 |author-link2= Michael O. Rabin
 |year= 1974
 |title= Super-Exponential Complexity of Presburger Arithmetic
 |url= http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps
 |series= SIAM-AMS Proceedings
 |editor-last= Karp
 |editor-first= Richard M.
 |book-title= Complexity of computation
 |publisher= [[American Mathematical Society]]
 |isbn= 978-0-8218-1327-0
 |oclc= 1205569621
 |volume= 7
 |pages= 27–41
 |access-date= 2006-06-11
 |archive-url= https://web.archive.org/web/20060915010325/http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps
 |archive-date= 2006-09-15
 |url-status= dead
}}

*{{cite journal
 |last1= Ginsburg
 |first1= Seymour
 |author-link1= Seymour Ginsburg
 |last2= Spanier
 |first2= Edwin Henry
 |author-link2= Edwin Spanier
 |year= 1966
 |title= Semigroups, Presburger Formulas, and Languages
 |journal= [[Pacific Journal of Mathematics]]
 |volume= 16
 |issue= 2
 |pages= 285–296
 |doi=10.2140/pjm.1966.16.285
 |doi-access=free
|url= https://projecteuclid.org/journals/pacific-journal-of-mathematics/volume-16/issue-2/Semigroups-Presburger-formulas-and-languages/pjm/1102994974.pdf
 }}

*{{cite conference
 | last= Haase
 | first= Christoph
 | year= 2014
 | title= Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
 | book-title= Proceedings CSL-[[Logic in Computer Science|LICS]]
 | publisher= ACM
 | pages= 47:1–47:10
 | doi= 10.1145/2603088.2603092
 | arxiv= 1401.5266
}}

*{{Cite journal
 |last= Haase
 |first= Christoph
 |year= 2018
 |title= A Survival Guide to Presburger Arithmetic
 |journal= ACM SIGLOG News
 |url= http://www.cs.ox.ac.uk/people/christoph.haase/home/publication/haa-18/haa-18.pdf
 |volume= 5
 |issue= 3
 |pages= 67–82
 |doi= 10.1145/3242953.3242964
 |s2cid= 51847374
}}

*{{cite web
 |last= Hoang
 |first= Nhat Minh
 |title= Presburger Arithmetic
 |url= https://www21.in.tum.de/teaching/sar/SS20/9.pdf
 |at= [[Technical University of Munich|Technische Universität München]]
 |quote= In this paper a procedure for constructing an automaton that decides Presburger arithmetic is explained.
 |access-date= 22 March 2024
}}

*{{cite book
 |last1= King
 |first1= Tim
 |last2= Barrett
 |first2= Clark W.
 |last3= Tinelli
 |first3= Cesare
 |title= 2014 Formal Methods in Computer-Aided Design (FMCAD)
 |year= 2014
 |chapter= Leveraging linear and mixed integer programming for SMT
 |volume= 2014
 |pages= 139–146
 |doi= 10.1109/FMCAD.2014.6987606
 |isbn= 978-0-9835-6784-4
 |s2cid= 5542629
}}

*{{cite journal
 |last1= Michaux
 |first1= Christian
 |last2= Villemaire
 |first2= Roger
 |title= Presburger Arithmetic and Recognizability of Sets of Natural Numbers by Automata: New Proofs of Cobham's and Semenov's Theorems
 |journal= [[Annals of Pure and Applied Logic]]
 |date= 1996
 |volume= 77
 |issue= 3
 |pages= 251–277
 |doi= 10.1016/0168-0072(95)00022-4
 |doi-access= 
}}

*{{Cite book
 |last= Monk
 |first= J. Donald
 |year= 2012
 |title= Mathematical Logic (Graduate Texts in Mathematics (37))
 |publisher= Springer
 |edition= Softcover reprint of the original 1st ed. 1976
 |isbn= 9781468494549
}}

*{{cite journal
 |last= Muchnik
 |first= Andrei A.
 |title= The definable criterion for definability in Presburger arithmetic and its applications
 |journal= Theor. Comput. Sci.
 |date= 2003
 |volume= 290
 |issue= 3
 |pages= 1433–1444
 |doi= 10.1016/S0304-3975(02)00047-6
 |doi-access= free
}}

*{{cite journal
 |last1= Nelson
 |first1= Greg
 |last2= Oppen
 |first2= Derek C.
 |date= April 1978
 |title= A simplifier based on efficient decision algorithms
 |journal= Proc. 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
 |pages= 141–150
 |doi= 10.1145/512760.512775
 |s2cid= 6342372
}}

*{{cite book
 |last1= Nguyen |first1= Danny
 |last2= Pak |first2= Igor |title= 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS)
 |chapter= Short Presburger Arithmetic is Hard
 |authorlink2=Igor Pak
 |year= 2017
 |pages= 37–48
 |chapter-url= http://www.math.ucla.edu/~pak/papers/hard_presburger3.pdf
 |access-date= 2022-09-04
 |arxiv= 1708.08179
 |doi= 10.1109/FOCS.2017.13 
|isbn= 978-1-5386-3464-6
 |s2cid= 3425421
 }}

*{{cite thesis
 |last= Nguyen Luu
 |first= Dahn
 |year= 2018
 |title= The Computational Complexity of Presburger Arithmetic
 |publisher= UCLA Electronic Theses and Dissertations
 |location= Los Angeles
 |url= https://escholarship.org/uc/item/6j9051vs
 |access-date= 2022-09-08
}}

*{{cite journal
 |last= Nipkow
 |first= T
 |year= 2010
 |title= Linear Quantifier Elimination
 |url= https://www.proof.cit.tum.de/~nipkow/pubs/jar10.pdf
 |journal= [[Journal of Automated Reasoning]]
 |volume= 45
 |issue= 2
 |pages= 189–212
 |doi= 10.1007/s10817-010-9183-0
 |s2cid= 14279141
}}

*{{cite journal
 |last= Oppen
 |first= Derek C.
 |year= 1978
 |title= A 2<sup>2<sup>2<sup>''pn''</sup></sup></sup> Upper Bound on the Complexity of Presburger Arithmetic
 |journal= [[J. Comput. Syst. Sci.]]
 |volume= 16
 |issue= 3
 |pages= 323–332
 |doi= 10.1016/0022-0000(78)90021-1
 |doi-access= free
}}

*{{cite journal
 |last= Presburger
 |first= Mojżesz
 |author-link= Mojżesz Presburger
 |date= 1929
 |title= Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt
 |journal= Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa
 |pages= 92–101
}}, see {{harvtxt|Stansifer|1984}} for an English translation

*{{cite conference
 |last= Pugh
 |first= William
 |author-link= William Pugh (computer scientist)
 |title= Proceedings of the 1991 ACM/IEEE conference on Supercomputing - Supercomputing '91
 |chapter= The Omega test: A fast and practical integer programming algorithm for dependence analysis
 |year= 1991
 |pages= 4–13
 |publisher = Association for Computing Machinery
 |publication-place= New York, NY, USA
 |doi= 10.1145/125826.125848
 |isbn= 0897914597
 |s2cid= 3174094
 |citeseerx= 10.1.1.37.1995
 }}

*{{cite conference
 |last1= Reddy
 |first1= C.R.
 |last2= Loveland
 |first2= D.W.
 |title= Proceedings of the tenth annual ACM symposium on Theory of computing - STOC '78
 |chapter= Presburger arithmetic with bounded quantifier alternation
 |year= 1978
 |pages = 320–325
 |doi= 10.1145/800133.804361
 |s2cid= 13966721
}}

*{{cite journal
 |first= A.L.
 |last= Semenov
 |year= 1977
 |title= Presburgerness of predicates regular in two number systems
 |language= ru
 |journal= [[Sibirsk. Mat. Zh.]]
 |volume= 18
 |issue= 2
 |pages= 403–418
|doi= 10.1007/BF00967164
 |bibcode= 1977SibMJ..18..289S
 }}

*{{cite report
 |last= Stansifer
 |first= Ryan
 |date= Sep 1984
 |title= Presburger's Article on Integer Arithmetic: Remarks and Translation
 |type= Technical Report
 |location= Ithaca/NY
 |publisher= Dept. of Computer Science, Cornell University
 |volume= TR84-639
 |url= http://cs.fit.edu/~ryan/papers/presburger.pdf
}}

*{{cite book
 |last= Young
 |first= P.
 |year= 1985
 |contribution= Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition
 |title= Recursion Theory, American Mathematical Society
 |editor= A. Nerode and R. Shore
 |pages= 503–522
}}

*{{cite thesis
 |last= Zoethout
 |first= Jetze
 |date= February 1, 2015
 |title= Interpretations in Presburger Arithmetic (Bachelor Thesis)
 |url= https://studenttheses.uu.nl/bitstream/handle/20.500.12932/20281/Thesis.pdf
 |access-date= 2023-08-25
 }}

{{Refend}}