file.pdf (216.52 kB)
0/0

Quantifier Elimination for the Reals with a Predicate for the Powers of Two

Download (216.52 kB)
journal contribution
posted on 01.01.2005 by Jeremy Avigad, Yimu Yin
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-theoretical argument, which provides no apparent bounds on the complexity of a decision procedure. We provide a syntactical argument that yields a procedure that is primitive recursive, although not elementary.

History

Publisher Statement

All Rights Reserved

Date

01/01/2005

Exports

Categories

Exports