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

DOI10.1007/978-3-319-21401-6_12zbMATH Open1465.03048arXiv1506.04863OpenAlexW1548563850MaRDI QIDQ3454091FDOQ3454091

Authors: Grant Olney Passmore 

Publication date: 2 December 2015

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

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (6)

• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• A conflict-driven solving procedure for poly-power constraints
• The existence of a near-unanimity term in a finite algebra is decidable

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)