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

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

Authors: Jeremy Avigad, Yimu Yin 

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

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

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

• Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
• Algorithms in real algebraic geometry
• Mathematical logic.
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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 (10)

• Semantics, specification logic, and Hoare logic of exact real computation
• Title not available (Why is that?)
• 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
• Computational complexity of quantifier-free negationless theory of field of rational numbers
• Real quantifier elimination is doubly exponential
• Title not available (Why is that?)
• 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)