Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers

Abstract

We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., $(x^n\in \mathbb{Q})$ and $(x^n\in \mathbb{Z})$. Our decision procedure combines computation over real algebraic cells with the rational root theorem and witness construction via algebraic number density arguments.

To appear in CADE-25: 25th International Conference on Automated Deduction, 2015. Proceedings to be published by Springer-Verlag