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

DOI10.1007/978-3-319-21401-6_12zbMath1465.03048arXiv1506.04863OpenAlexW1548563850MaRDI QIDQ3454091

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)

Related Items (1)

A conflict-driven solving procedure for poly-power constraints

Uses Software

• Isabelle
• MetiTarski

Cites Work

• Unnamed Item
• Unnamed Item
• Factoring polynomials and the knapsack problem
• 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
• The field of reals with a predicate for the powers of two
• Isabelle. A generic theorem prover
• Towards faster real algebraic numbers
• MetiTarski: Past and Future
• Characterizing integers among rational numbers with a universal-existential formula
• Factorisation of $x^N - q$ over Q
• Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
• A formally verified proof of the prime number theorem
• Algorithms in real algebraic geometry

This page was built for publication: Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers