English

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

Logic 2015-06-17 v1 Logic in Computer Science

Abstract

We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., (xnQ)(x^n \in \mathbb{Q}) and (xnZ)(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.

Keywords

Cite

@article{arxiv.1506.04863,
  title  = {Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers},
  author = {Grant Olney Passmore},
  journal= {arXiv preprint arXiv:1506.04863},
  year   = {2015}
}

Comments

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

R2 v1 2026-06-22T09:54:18.858Z