Decidability of univariate real algebra with predicates for rational and integer powers

DOI10.1007/978-3-319-21401-6_12MaRDI QIDQ3454091zbMATH OpenOpenAlexFDO

Authors Grant Olney Passmore

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1506.04863

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Real algebra (13J30)

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

Recommendations

• On the decidability of the real field with a generic power function
• Decidability of the rings of real algebraic and p-adic algebraic integers.
• Quantifier elimination for the reals with a predicate for the powers of two
• Combining decision procedures for the reals
• scientific article; zbMATH DE number 4150340

Cites work

• scientific article; zbMATH DE number 517393 (Why is no real title available?)
• scientific article; zbMATH DE number 545277 (Why is no real title available?)
• A formally verified proof of the prime number theorem
• Algorithms in real algebraic geometry
• Characterizing integers among rational numbers with a universal-existential formula
• Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
• Computing partial information out of intractable: powers of algebraic numbers as an example
• Factoring polynomials and the knapsack problem
• Factorisation of $x^N - q$ over Q
• Isabelle. A generic theorem prover
• MetiTarski: past and future
• Quantifier elimination for the reals with a predicate for the powers of two
• The field of reals with a predicate for the powers of two
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Towards faster real algebraic numbers

Cited in

(6)

• A conflict-driven solving procedure for poly-power constraints
• The existence of a near-unanimity term in a finite algebra is decidable
• scientific article; zbMATH DE number 6930595 (Why is no real title available?)
• scientific article; zbMATH DE number 177484 (Why is no real title available?)
• On the decidability of the real field with a generic power function
• The field of reals with a predicate for the real algebraic numbers and a predicate for the integer powers of two

Describes a project that uses

Uses Software

• Isabelle
• MetiTarski

This page was built for publication: Decidability of univariate real algebra with predicates for rational and integer powers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3454091)