Publication:868941

DOI10.1016/J.TCS.2006.10.005zbMATH Open1113.03027arXivcs/0610117OpenAlexW2126527995MaRDI QIDQ868941FDOQ868941

Yimu Yin, Jeremy Avigad

Publication date: 26 February 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

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

Full work available at URL: https://arxiv.org/abs/cs/0610117

zbMATH Keywords

quantifier eliminationreal closed fields

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Model theory of fields (12L12) Quantifier elimination, model completeness, and related topics (03C10)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
• Algorithms in real algebraic geometry
• Mathematical logic.
• THE FIELDS OF REAL AND COMPLEX NUMBERS WITH A SMALL MULTIPLICATIVE GROUP
• New results on quantifier elimination over real closed fields and applications to constraint databases
• The computational complexity of logical theories
• The field of reals with a predicate for the powers of two
• The complexity of almost linear diophantine problems
• Alfred Tarski's elimination theory for real closed fields
• Expansions of o-minimal structures by fast sequences

Cited In (7)

• Semantics, specification logic, and Hoare logic of exact real computation
• Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
• Title not available (Why is that?)
• A generalization of Cobham's theorem to automata over real numbers
• Computer Science for Continuous Data
• Real quantifier elimination is doubly exponential
• Title not available (Why is that?)

This page was built for publication: Quantifier elimination for the reals with a predicate for the powers of two

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q868941)