Quantifier elimination for the reals with a predicate for the powers of two

2006/10/19 by Jeremy Avigad, Avigad, Jeremy, Yimu Yin +1
Computer Science · Mathematics · #Computability, Logic, AI Algorithms #Advanced Topology and Set Theory #Logic, Reasoning, and Knowledge

paper · pdf · doi:10.48550/arxiv.cs/0610117

Abstract

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⁰_O(n), where n is the length of the input formula and 2_k^x denotes k-fold iterated exponentiation.

Related

• An efficient quantifier elimination procedure for Presburger arithmetic
• Lecture notes on complexity of quantifier elimination over the reals
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• On elimination of quantifiers in some non-classical mathematical theories
• Iterated Resultants and Rational Functions in Real Quantifier Elimination