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., and . 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