Speedups for Presburger Arithmetic and Real Closed Fields
In the present paper, we consider Presburger arithmetic PrA and the theory of real closed fields RCF. Due to quantifier elimination in these theories, there are two kinds of natural ways to axiomatize them. Namely, on one hand, PrA can be axiomatized with the full schema of first-order induction, and RCF with the full schema of the first-order least upper bound principle. At the same time, there are natural axiomatizations of these theories that avoid the use of formulas of unbounded quantifier depth. In the present paper, we compare these two groups of axiomatizations from the perspective…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2603.00642
curl -X POST /api/v1/records/arxiv/2603.00642/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2603.00642/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'