The DOI matches its Crossref record, with a small difference in title or year.
Super-Exponential Complexity of Presburger Arithmetic
Open accessAbstract
Lower bounds are established on the computational complexity of the decision problem and on the inherent lengths of proofs for two classical decidable theories of logic: the first-order theory of the real numbers under addition, and Presburger arithmetic — the first-order theory of addition on the natural numbers. There is a fixed constant c > 0 such that for every (nondeterministic) decision procedure for determining the truth of sentences of real addition and for all sufficiently large n, there is a sentence of length n for which the decision procedure runs for more than 2 cn steps. In the case of Presburger arithmetic, the corresponding bound is \({2^{{2^{cn}}}}\). These bounds apply also to the minimal lengths of proofs for any complete axiomatization in which the axioms are easily recognized.
Overview
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
The cited source says what the claim attributes to it.
In the citing paper
“| O ( n k ) time bounded LLMs | Presburger Arithmetic [56, 65] | Requiring Ω(2 2 cn ) solution [18] | None |”
From Hallucination is Inevitable: An Innate Limitation of Large Language Models (2024) · cites this paper as [18]
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Citations
Cites
Still being checked.
Research works printed but not linked: 4
- J. Ferrante and C. Rackoff, "A decision procedure for the first order theory of real addition with order," Project MAC Technical Memorandum 33, M.I.T., Cambridge, Mass. (May 1973), 16 pp.
- M. Presburger, "Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt", Comptes-rendus du I Congres des Mathematiciens des Pays Slaves, Warsaw (1930), pp. 92-101, 395.
- A. Tarski(with the assistance of J.C.C. McKinsey), A Decision Method •for Elementary Algebra and Geometry, 2nd ed., University of California Press, Berkeley and Los Angeles, 1951. l l. Report No~, GJJ 46 71 + N00014-1 2 • 70-A-0362-0003 ~1~~ iN-41
- Michael J. Fischer and Michael O. Rabin 9. Pcrfmrning Organization Name and Address PROJECT MAC; MASSACHUSETTS INSTITUTE OF TECHNOLOGY: 545 Technology Square, Cambridge, Massachusetts 02139
Cited by
A logic for reasoning about probabilities
Fagin, R., Halpern, J. Y., & Megiddo, N. (1990) · Information and Computation · doi:10.1016/0890-5401(90)90060-u · Cited by 584
Computation in networks of passively mobile finite-state sensors
Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M. J., & Peralta, R. (2005) · Distributed Computing · doi:10.1007/s00446-005-0138-3 · Cited by 587
Self-citationThe Complexity of Optimal Queuing Network Control
Papadimitriou, C. H., & Tsitsiklis, J. N. (1999) · Mathematics of Operations Research · doi:10.1287/moor.24.2.293 · Cited by 469
Graph-theoretic arguments in low-level complexity
Valiant, L. G. (1977) · Lecture Notes in Computer Science · doi:10.1007/3-540-08353-7_135 · Cited by 312
Definability and fast quantifier elimination in algebraically closed fields
Heintz, J. (1983) · Theoretical Computer Science · doi:10.1016/0304-3975(83)90002-6 · Cited by 318
Metadata
- Authors
- Fischer, M. J., & Rabin, M. O.
- ORCID
- Fischer, Michael J.
- Venue
- Texts and Monographs in Symbolic Computation
- Publisher
- Springer Vienna
- Published
- 1998
- Pages
- 122-135
- ISSN
- 0943-853X (ISSN-L)
- OpenAlex
- W1556844982
- Cited by
- 331
- References
- 0
- Citations by year
- 2026: 2 · 2025: 2 · 2024: 1 · 2023: 5 · 2022: 3 · 2021: 10 · 2020: 4 · 2019: 6 · 2018: 8 · 2017: 10 · 2016: 8 · 2015: 5 · 2014: 11 · 2013: 6 · 2012: 7
- FWCI
- 16.40
- Type
- book chapter
- Language
- en
- Open access
- green
- hdl.handle.net
- Licence
- cc-by-nc
- Locations
- Texts & monographs in symbolic computation/Texts and monographs in symbolic computation (publishedVersion)
- DSpace@MIT (Massachusetts Institute of Technology) (submittedVersion, cc-by-nc)
- Funders
- Hebrew University of Jerusalem
- University of Toronto
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › semigroups and automata theory
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Computability, Logic, AI Algorithms
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Complexity and Algorithms in Graphs
- Keywords
- Presburger arithmetic, lower bounds, computational complexity, decision problems, proof length, proof complexity, axiomatization
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
How to cite
Cite CoChat for the checks on this page, and the paper for its own findings.
- This page
- CoChat. (2026). Citation check: Super-Exponential Complexity of Presburger Arithmetic. https://app.cochat.ai/papers/10.1007/978-3-7091-9459-1_5
- The paper
- Fischer, M. J., & Rabin, M. O. (1998). Super-Exponential Complexity of Presburger Arithmetic. Texts and Monographs in Symbolic Computation. https://doi.org/10.1007/978-3-7091-9459-1_5
Data sources
Bibliographic data: Semantic Scholar, OpenAlex, Crossref.
Contains information from the Semantic Scholar Academic Graph Datasets, made available under the ODC Attribution License (ODC-BY 1.0).
Semantic Scholar’s data is described in: Kinney, R., et al. (2023). The Semantic Scholar Open Data Platform. arXiv:2301.10140.
