Quantifier elimination for the reals with a predicate for the powers of two
| dc.creator | Avigad, Jeremy | |
| dc.creator | Yin, Yimu | |
| dc.date | 2006-10-19 | |
| dc.date.accessioned | 2026-07-07T07:27:53Z | |
| dc.date.available | 2026-07-07T07:27:53Z | |
| dc.description | In 1985, van den Dries showed that the theory of the reals with a predicate for the integer powers of two admits quantifier elimination in an expanded language, and is hence decidable. He gave a model-theoretic argument, which provides no apparent bounds on the complexity of a decision procedure. We provide a syntactic argument that yields a procedure that is primitive recursive, although not elementary. In particular, we show that it is possible to eliminate a single block of existential quantifiers in time $2^0_{O(n)}$, where $n$ is the length of the input formula and $2_k^x$ denotes $k$-fold iterated exponentiation. | |
| dc.identifier | https://arxiv.org/abs/cs/0610117 | |
| dc.identifier | http://arxiv.org/abs/cs/0610117 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/117537 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.4.1; I.2.3 | |
| dc.title | Quantifier elimination for the reals with a predicate for the powers of two | |
| dc.type | text |