Skip to main content
SpringerLink
Log in

A Proof-Producing Decision Procedure for Real Arithmetic

  • Conference paper
Automated Deduction – CADE-20 (CADE 2005)

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

Included in the following conference series:

Abstract

We present a fully proof-producing implementation of a quantifier elimination procedure for real closed fields. To our knowledge, this is the first generally useful proof-producing implementation of such an algorithm. While many problems within the domain are intractable, we demonstrate convincing examples of its value in interactive theorem proving.

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

Access this chapter

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barrett, C., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Blum, M.: Program result checking: A new approach to making programs more reliable. In: Lingas, A., Carlsson, S., Karlsson, R. (eds.) ICALP 1993. LNCS, vol. 700, pp. 1–14. Springer, Heidelberg (1993)

    Google Scholar 

  3. Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry. In: Ergebnisse der Mathematik und ihrer Grenzgebiete, vol. 36, Springer, Heidelberg (1998)

    Google Scholar 

  4. Boulton, R.J.: Efficiency in a fully-expansive theorem prover. Technical Report 337, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, Author’s PhD thesis (1993)

    Google Scholar 

  5. Caviness, B.F., Johnson, J.R.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and monographs in symbolic computation. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  6. Cohen, P.J.: Decision procedures for real and p-adic fields. Communications in Pure and Applied Mathematics 22, 131–151 (1969)

    Article  MATH  Google Scholar 

  7. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Second GI Conference on Automata Theory and Formal Languages, Kaiserslautern. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1976)

    Google Scholar 

  8. Davis, M.: A computer program for Presburger’s algorithm. In: Summaries of talks presented at the Summer Institute for Symbolic Logic, Cornell University, Institute for Defense Analyses, Princeton, NJ, pp. 215–233 (1957); Reprinted in [78], pp. 41–48

    Google Scholar 

  9. Engeler, E.: Foundations of Mathematics: Questions of Analysis, Geometry and Algorithmics, Original German edn., Metamathematik der Elementarmathematik, Series Hochschultext. Springer, Heidelberg (1993)

    Google Scholar 

  10. Gårding, L.: Some Points of Analysis and Their History, volume 11 of University Lecture Series. American Mathematical Society / Higher Education Press (1997)

    Google Scholar 

  11. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  12. Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979)

    Google Scholar 

  13. Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995), Available on the Web as, http://www.cl.cam.ac.uk/users/jrh/papers/reflect.dvi.gz

  14. Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  15. Harrison, J.: Theorem Proving with the Real Numbers. Springer-Verlag, Revised version of author’s PhD thesis (1998)

    Google Scholar 

  16. Harrison, J.: Complex quantifier elimination in HOL. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. Published as Informatics Report Series EDI-INF-RR-0046, pp. 159–174. University of Edinburgh (2001), Available on the Web at http://www.informatics.ed.ac.uk/publications/report/0046.html

  17. Hörmander, L.: The Analysis of Linear Partial Differential Operators II. In: Grundlehren der mathematischen Wissenschaften, vol. 257, Springer, Heidelberg (1983)

    Google Scholar 

  18. Hunt, W.A., Krug, R.B., Moore, J.: Linear and nonlinear arithmetic in ACL2. In: Geist, D. (ed.) CHARME 2003. LNCS, vol. 2860, pp. 319–333. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  19. Kreisel, G., Krivine, J.-L.: Elements of mathematical logic: model theory, revised 2nd edn. (1971), 1st edn. (1967). Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1971); Translation of the French ‘Eléments de logique mathématique, théorie des modeles’ published by Dunod, Paris (1964)

    Google Scholar 

  20. Kumar, R., Kropf, T., Schneider, K.: Integrating a first-order automatic prover in the HOL environment. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications, University of California at Davis, Davis CA, USA, pp. 170–176. IEEE Computer Society Press, Los Alamitos (1991)

    Chapter  Google Scholar 

  21. Mahboubi, A., Pottier, L.: Elimination des quantificateurs sur les réels en Coq. In: Journées Francophones des Langages Applicatifs (JFLA), available on the Web (2002), from http://pauillac.inria.fr/jfla/2002/actes/index.html08-mahboubi.ps

  22. Michaux, C., Ozturk, A.: Quantifier elimination following Muchnik. Université de Mons-Hainaut, Institute de Mathématique, Preprint 10, http://w3.umh.ac.be/math/preprints/src/Ozturk020411.pdf

  23. Necula, G.C.: Proof-carrying code. In: Conference record of POPL 1997: the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106–119. ACM Press, New York (1997)

    Chapter  Google Scholar 

  24. Parrilo, P.: Semidefinite programming relaxations for semialgebraic problems. Available from the Web (2001), at http://citeseer.nj.nec.com/parrilo01semidefinite.html

  25. Paulson, L.C.: Isabelle: a generic theorem prover. LNCS, vol. 828. Springer, Heidelberg (1994); (With contributions by Tobias Nipkow)

    Book  MATH  Google Scholar 

  26. Schoutens, H.: Muchnik’s proof of Tarski-Seidenberg. Notes (2001), available from http://www.math.ohio-state.edu/~schoutens/PDF/Muchnik.pdf

  27. Seidenberg, A.: A new decision method for elementary algebra. Annals of Mathematics 60, 365–374 (1954)

    Article  MathSciNet  Google Scholar 

  28. Siekmann, J., Wrightson, G.: Automation of Reasoning — Classical Papers on Computational Logic (1957-1966), vol. I. Springer, Heidelberg (1983)

    Google Scholar 

  29. Sturm, C.: Mémoire sue la résolution des équations numériques. Mémoire des Savants Etrangers 6, 271–318 (1835)

    Google Scholar 

  30. Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Previous version published as a technical report by the RAND Corporation, (1948); prepared for publication by J. C. C. McKinsey. Reprinted In: [5], pp. 24–84 (1951)

    Google Scholar 

  31. Vorobjov, N.N.: Deciding consistency of systems of polynomial in exponent inequalities in subexponential time. In: Mora, T., Traverso, C. (eds.) Proceedings of the MEGA-90 Symposium on Effective Methods in Algebraic Geometry, Castiglioncello, Livorno, Italy. Progress in Mathematics, vol. 94, pp. 491–500. Birkhäuser, Basel (1990)

    Google Scholar 

  32. Weispfenning, V.: Quantifier elimination for real algebra — the quadratic case and beyond. Applicable Algebra in Engineering Communications and Computing 8, 85–101 (1997)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Carnegie-Mellon University, 5000 Forbes Avenue, Pittsburgh, PA, 15213, USA

    Sean McLaughlin

  2. Intel Corporation, JF1-13, Hillsboro, OR, 97124, USA

    John Harrison

Authors
  1. Sean McLaughlin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Harrison
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technical University of Catalonia, Barcelona

    Robert Nieuwenhuis

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

McLaughlin, S., Harrison, J. (2005). A Proof-Producing Decision Procedure for Real Arithmetic. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_22

Download citation

  • DOI: https://doi.org/10.1007/11532231_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28005-7

  • Online ISBN: 978-3-540-31864-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation