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

We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., “xn ∈ Q” and “xn ∈ Z.” Our decision procedure combines computation over real algebraic cells with the rational root theorem and witness construction via algebraic number density arguments.

• Type: Journal
• Year: 2015
• Where: CADE
• Authors: Grant Olney Passmore
• Keywords: CADE 2015, Logical Reasoning