{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:48:30Z","timestamp":1767926910776,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540280057","type":"print"},{"value":"9783540318644","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_22","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"295-314","source":"Crossref","is-referenced-by-count":35,"title":["A Proof-Producing Decision Procedure for Real Arithmetic"],"prefix":"10.1007","author":[{"given":"Sean","family":"McLaughlin","sequence":"first","affiliation":[]},{"given":"John","family":"Harrison","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"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.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Automata, Languages and Programming","author":"M. Blum","year":"1993","unstructured":"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.\u00a0700, pp. 1\u201314. Springer, Heidelberg (1993)"},{"key":"22_CR3","volume-title":"Ergebnisse der Mathematik und ihrer Grenzgebiete","author":"J. Bochnak","year":"1998","unstructured":"Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry. In: Ergebnisse der Mathematik und ihrer Grenzgebiete, vol.\u00a036, Springer, Heidelberg (1998)"},{"key":"22_CR4","unstructured":"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\u2019s PhD thesis (1993)"},{"key":"22_CR5","series-title":"Texts and monographs in symbolic computation","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-7091-9459-1","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","author":"B.F. Caviness","year":"1998","unstructured":"Caviness, B.F., Johnson, J.R.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and monographs in symbolic computation. Springer, Heidelberg (1998)"},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1002\/cpa.3160220202","volume":"22","author":"P.J. Cohen","year":"1969","unstructured":"Cohen, P.J.: Decision procedures for real and p-adic fields. Communications in Pure and Applied Mathematics\u00a022, 131\u2013151 (1969)","journal-title":"Communications in Pure and Applied Mathematics"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","first-page":"134","volume-title":"Second GI Conference on Automata Theory and Formal Languages","author":"G.E. Collins","year":"1976","unstructured":"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.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1976)"},{"key":"#cr-split#-22_CR8.1","unstructured":"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);"},{"key":"#cr-split#-22_CR8.2","unstructured":"Reprinted in [78], pp. 41???48"},{"key":"22_CR9","unstructured":"Engeler, E.: Foundations of Mathematics: Questions of Analysis, Geometry and Algorithmics, Original German edn., Metamathematik der Elementarmathematik, Series Hochschultext. Springer, Heidelberg (1993)"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"G\u00e5rding, L.: Some Points of Analysis and Their History, volume\u00a011 of University Lecture Series. American Mathematical Society \/ Higher Education Press (1997)","DOI":"10.1090\/ulect\/011"},{"key":"22_CR11","volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"22_CR13","unstructured":"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"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer-Verlag, Revised version of author\u2019s PhD thesis (1998)","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"22_CR16","unstructured":"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\u2013174. University of Edinburgh (2001), Available on the Web at http:\/\/www.informatics.ed.ac.uk\/publications\/report\/0046.html"},{"key":"22_CR17","volume-title":"Grundlehren der mathematischen Wissenschaften","author":"L. H\u00f6rmander","year":"1983","unstructured":"H\u00f6rmander, L.: The Analysis of Linear Partial Differential Operators II. In: Grundlehren der mathematischen Wissenschaften, vol.\u00a0257, Springer, Heidelberg (1983)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-39724-3_29","volume-title":"Correct Hardware Design and Verification Methods","author":"W.A. Hunt","year":"2003","unstructured":"Hunt, W.A., Krug, R.B., Moore, J.: Linear and nonlinear arithmetic in ACL2. In: Geist, D. (ed.) CHARME 2003. LNCS, vol.\u00a02860, pp. 319\u2013333. Springer, Heidelberg (2003)"},{"key":"#cr-split#-22_CR19.1","unstructured":"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);"},{"key":"#cr-split#-22_CR19.2","unstructured":"Translation of the French ???El??ments de logique math??matique, th??orie des modeles??? published by Dunod, Paris (1964)"},{"key":"22_CR20","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/HOL.1991.596284","volume-title":"Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications","author":"R. Kumar","year":"1991","unstructured":"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\u2013176. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"22_CR21","unstructured":"Mahboubi, A., Pottier, L.: Elimination des quantificateurs sur les r\u00e9els en Coq. In: Journ\u00e9es Francophones des Langages Applicatifs (JFLA), available on the Web (2002), from http:\/\/pauillac.inria.fr\/jfla\/2002\/actes\/index.html08-mahboubi.ps"},{"key":"22_CR22","unstructured":"Michaux, C., Ozturk, A.: Quantifier elimination following Muchnik. Universit\u00e9 de Mons-Hainaut, Institute de Math\u00e9matique, Preprint 10, http:\/\/w3.umh.ac.be\/math\/preprints\/src\/Ozturk020411.pdf"},{"key":"22_CR23","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Conference record of POPL 1997: the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"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\u2013119. ACM Press, New York (1997)"},{"key":"22_CR24","unstructured":"Parrilo, P.: Semidefinite programming relaxations for semialgebraic problems. Available from the Web (2001), at http:\/\/citeseer.nj.nec.com\/parrilo01semidefinite.html"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: a generic theorem prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994); (With contributions by Tobias Nipkow)"},{"key":"22_CR26","unstructured":"Schoutens, H.: Muchnik\u2019s proof of Tarski-Seidenberg. Notes (2001), available from http:\/\/www.math.ohio-state.edu\/~schoutens\/PDF\/Muchnik.pdf"},{"key":"22_CR27","doi-asserted-by":"publisher","first-page":"365","DOI":"10.2307\/1969640","volume":"60","author":"A. Seidenberg","year":"1954","unstructured":"Seidenberg, A.: A new decision method for elementary algebra. Annals of Mathematics\u00a060, 365\u2013374 (1954)","journal-title":"Annals of Mathematics"},{"key":"22_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-81955-1","volume-title":"Automation of Reasoning \u2014 Classical Papers on Computational Logic (1957-1966)","author":"J. Siekmann","year":"1983","unstructured":"Siekmann, J., Wrightson, G.: Automation of Reasoning \u2014 Classical Papers on Computational Logic (1957-1966), vol.\u00a0I. Springer, Heidelberg (1983)"},{"key":"22_CR29","unstructured":"Sturm, C.: M\u00e9moire sue la r\u00e9solution des \u00e9quations num\u00e9riques. M\u00e9moire des Savants Etrangers\u00a06, 271\u2013318 (1835)"},{"key":"22_CR30","unstructured":"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\u201384 (1951)"},{"key":"22_CR31","series-title":"Progress in Mathematics","first-page":"491","volume-title":"Proceedings of the MEGA-90 Symposium on Effective Methods in Algebraic Geometry","author":"N.N. Vorobjov","year":"1990","unstructured":"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.\u00a094, pp. 491\u2013500. Birkh\u00e4user, Basel (1990)"},{"key":"22_CR32","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V. Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra \u2014 the quadratic case and beyond. Applicable Algebra in Engineering Communications and Computing\u00a08, 85\u2013101 (1997)","journal-title":"Applicable Algebra in Engineering Communications and Computing"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T06:57:31Z","timestamp":1685689051000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/11532231_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}