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

DOI10.1016/J.TCS.2006.10.005MaRDI QIDQ868941zbMATH OpenOpenAlexFDO

Authors Jeremy Avigad, Yimu Yin

Publication date 26 February 2007

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

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)

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.

Recommendations

• Real quantifier elimination is doubly exponential
• The field of reals with a predicate for the powers of two
• On the computational complexity and geometry of the first-order theory of the reals. III: Quantifier elimination
• scientific article; zbMATH DE number 4008374
• Quantifier elimination for real algebra -- the quadratic case and beyond

Cites work

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

Cited in

(10)

• Semantics, specification logic, and Hoare logic of exact real computation
• scientific article; zbMATH DE number 1775408 (Why is no real title available?)
• A generalization of Cobham's theorem to automata over real numbers
• Computer Science for Continuous Data
• Decidability of univariate real algebra with predicates for rational and integer powers
• The field of reals with a predicate for the powers of two
• Real quantifier elimination is doubly exponential
• Computational complexity of quantifier-free negationless theory of field of rational numbers
• scientific article; zbMATH DE number 1302474 (Why is no real title available?)
• Structure with fast elimination of quantifiers

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)