Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 2015: Automated Deduction - CADE-25 pp 181–196Cite as

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

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9195))

Abstract

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

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    In fact, the completeness proof shows that rule 3 is logically unnecessary. Nevertheless, we find its inclusion in the saturation process useful in practice.

  2. 2.

    The implementation of our procedure, including computations over r-cells, \({\varGamma }\)-saturation and the proof output routines can be found in the RCF/ modules in the MetiTarski source code at http://metitarski.googlecode.com/.

References

  1. Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comp. Logic vol. 9(1), Article No. 2 (2007)

    Google Scholar 

  2. Avigad, J., Yin, Y.: Quantifier elimination for the reals with a predicate for the powers of two. Theor. Comput. Sci. 370, 1–3 (2007)

    Article  MathSciNet  Google Scholar 

  3. Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Springer, Secaucus (2006)

    MATH  Google Scholar 

  4. Collins, G.E., Akritas, A.G.: Polynomial real root isolation using Descarte’s rule of signs. In: ACM Symposium on Symbolic and Algebraic computation. ACM (1976)

    Google Scholar 

  5. van den Dries, L.: The field of reals with a predicate for the powers of two. Manuscr. Math. 54(1–2), 187–195 (1985)

    Article  Google Scholar 

  6. Hirvensalo, M., Karhumäki, J., Rabinovich, A.: Computing partial information out of intractable: powers of algebraic numbers as an example. J. Number Theor. 130(2), 232–253 (2010)

    Article  MATH  Google Scholar 

  7. van Hoeij, M.: Factoring polynomials and the knapsack problem. J. Number Theor. 95(2), 167–189 (2002)

    Article  MATH  Google Scholar 

  8. Hollmann, H.: Factorisation of \(x^n - q\) over Q. Acta Arith. 45(4), 329–335 (1986)

    MathSciNet  MATH  Google Scholar 

  9. Koenigsmann, J.: Defining \(\mathbb{Z}\) in \(\mathbb{Q}\). Annals of Mathematics, To appear (2015)

    Google Scholar 

  10. Koenigsmann, J.: Personal communication (2015)

    Google Scholar 

  11. Matiyasevich, Y.: Hilbert’s Tenth Problem. MIT Press, Cambridge (1993)

    Google Scholar 

  12. Mishra, B.: Algorithmic Algebra. Springer, New York (1993)

    Book  MATH  Google Scholar 

  13. de Moura, L., Passmore, G.O.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 178–192. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  14. Paulson, L.C.: Isabelle: A Generic Theorem Prover, vol. 828. Springer, New York (1994)

    Book  MATH  Google Scholar 

  15. Paulson, L.C.: MetiTarski: past and future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 1–10. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  16. Poonen, B.: Characterizing integers among rational numbers with a universal-existential formula. Am. J. Math. 131(3), 675–682 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  17. Rioboo, R.: Towards faster real algebraic numbers. J. Sym. Comp. 36(3–4), 513–533 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  18. Robinson, J.: Definability and Decision Problems in Arithmetic. Ph.D. thesis, University of California, Berkeley (1948)

    Google Scholar 

  19. Uspensky, J.V.: Theory of Equations. McGraw-Hill, New York (1948)

    Google Scholar 

  20. Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: ISSAC 1999, New York, NY, USA (1999)

    Google Scholar 

  21. Wiedijk, F.: The Seventeen Provers of the World. Springer, New York (2006)

    Book  Google Scholar 

Download references

Acknowledgements

We thank Jeremy Avigad, Wenda Li, Larry Paulson, András Salamon and the anonymous referees for their helpful comments.

Author information

Authors and Affiliations

  1. Aesthetic Integration, London and Clare Hall, University of Cambridge, Cambridge, England

    Grant Olney Passmore

Authors
  1. Grant Olney Passmore
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Grant Olney Passmore .

Editor information

Editors and Affiliations

  1. University of Ottawa, Ottawa, Canada

    Amy P. Felty

  2. University of Innsbruck, Innsbruck, Austria

    Aart Middeldorp

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Passmore, G.O. (2015). Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers. In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-21401-6_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-21400-9

  • Online ISBN: 978-3-319-21401-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation