{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T11:53:47Z","timestamp":1773143627357,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540745907","type":"print"},{"value":"9783540745914","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_9","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"102-118","source":"Crossref","is-referenced-by-count":43,"title":["Verifying Nonlinear Real Formulas Via Sums of Squares"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Akbarpour, B., Paulson, L.C.: Towards automatic proofs of inequalities involving elementary functions. In: Cook, B., Sebastiani, R. (eds.) Proceedings of PDPAR 2006: Pragmatics of Decision Procedures in Automated Reasoning, pp. 27\u201337 (2006)"},{"key":"9_CR2","unstructured":"Akg\u00fcl, M.: Topics in relaxation and ellipsoidal methods. Research notes in mathematics, vol.\u00a097. Pitman (1984)"},{"key":"9_CR3","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/BF02952513","volume":"5","author":"E. Artin","year":"1927","unstructured":"Artin, E.: \u00dcber die Zerlegung definiter Funktionen in Quadrate. Hamburg Abhandlung\u00a05, 100\u2013115 (1927)","journal-title":"Hamburg Abhandlung"},{"key":"9_CR4","unstructured":"Avigad, J., Friedman, H.: Combining decision procedures for the reals. Logical Methods in Computer Science (to appear), available online at http:\/\/arxiv.org\/abs\/cs.LO\/0601134"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"1309","DOI":"10.1109\/81.883325","volume":"47","author":"S. Basu","year":"2000","unstructured":"Basu, S.: A constructive algorithm for 2-D spectral factorization with rational spectral factors. IEEE Transactions on Circuits and Systems\u2013I: Fundamental Theory and Applications\u00a047, 1309\u20131318 (2000)","journal-title":"IEEE Transactions on Circuits and Systems\u2013I: Fundamental Theory and Applications"},{"key":"9_CR6","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1080\/10556789908805765","volume":"11","author":"B. Borchers","year":"1999","unstructured":"Borchers, B.: CSDP: A C library for semidefinite programming. Optimization Methods and Software\u00a011, 613\u2013623 (1999)","journal-title":"Optimization Methods and Software"},{"key":"9_CR7","series-title":"Texts and monographs in symbolic computation","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","year":"1998","unstructured":"Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and monographs in symbolic computation. Springer, Heidelberg (1998)"},{"key":"9_CR8","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":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"9_CR10","volume-title":"Algebra: a text-book of determinants, matrices, and algebraic forms","author":"W.L. Ferrar","year":"1957","unstructured":"Ferrar, W.L.: Algebra: a text-book of determinants, matrices, and algebraic forms, 2nd edn. Oxford University Press, Oxford (1957)","edition":"2"},{"key":"9_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-78240-4","volume-title":"Geometric algorithms and combinatorial optimization","author":"M. Grotschel","year":"1993","unstructured":"Grotschel, M., Lovsz, L., Schrijver, A.: Geometric algorithms and combinatorial optimization. Springer, Heidelberg (1993)"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/S0747-7171(03)00073-7","volume":"37","author":"Z. Guangxing","year":"2004","unstructured":"Guangxing, Z., Xiaoning, Z.: An effective decision method for semidefinite polynomials. Journal of Symbolic Computation\u00a037, 83\u201399 (2004)","journal-title":"Journal of Symbolic Computation"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/BFb0028391","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1997","unstructured":"Harrison, J.: Verifying the accuracy of polynomial approximations in HOL. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 137\u2013152. Springer, Heidelberg (1997)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-40922-X_14","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"2000","unstructured":"Harrison, J.: Formal verification of floating point trigonometric functions. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 217\u2013233. Springer, Heidelberg (2000)"},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A sceptic\u2019s approach to combining HOL and Maple. Journal of Automated Reasoning\u00a021, 279\u2013294 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BF01443605","volume":"32","author":"D. Hilbert","year":"1888","unstructured":"Hilbert, D.: \u00dcber die Darstellung definiter Formen als Summe von Formenquadraten. Mathematische Annalen\u00a032, 342\u2013350 (1888)","journal-title":"Mathematische Annalen"},{"key":"9_CR17","series-title":"Grundlehren der mathematischen Wissenschaften","volume-title":"The Analysis of Linear Partial Differential Operators II","year":"1983","unstructured":"H\u00f6rmander, L. (ed.): The Analysis of Linear Partial Differential Operators II. Grundlehren der mathematischen Wissenschaften, vol.\u00a0257. Springer, Heidelberg (1983)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 319\u2013333. Springer, Heidelberg (2003)"},{"key":"9_CR19","volume-title":"Basic Algebra II","author":"N. Jacobson","year":"1989","unstructured":"Jacobson, N.: Basic Algebra II, 2nd edn. W. H. Freeman, New York (1989)","edition":"2"},{"key":"9_CR20","first-page":"191","volume":"20","author":"L.G. Khachian","year":"1979","unstructured":"Khachian, L.G.: A polynomial algorithm in linear programming. Soviet Mathematics Doklady\u00a020, 191\u2013194 (1979)","journal-title":"Soviet Mathematics Doklady"},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/BF01449981","volume":"62","author":"E. Landau","year":"1906","unstructured":"Landau, E.: \u00dcber die Darstellung definiter Funktionen durch Quadrate. Mathematischen Annalen\u00a062, 272\u2013285 (1906)","journal-title":"Mathematischen Annalen"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Lombardi, H.: Effective real nullstellensatz and variants. 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. 263\u2013288. Birkh\u00e4user, Basel (1990)","DOI":"10.1007\/978-1-4612-0441-1_18"},{"key":"9_CR23","unstructured":"Mahboubi, A., Pottier, L.: Elimination des quantificateurs sur les r\u00e9els en Coq. In: Journ\u00e9es Francophones des Langages Applicatifs (JFLA) (2002), available on the Web from http:\/\/pauillac.inria.fr\/jfla\/2002\/actes\/index.html08-mahboubi.ps"},{"key":"9_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/11532231_22","volume-title":"Automated Deduction \u2013 CADE-20","author":"S. McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, pp. 295\u2013314. Springer, Heidelberg (2005)"},{"key":"9_CR25","volume-title":"Inequalities","author":"T.S. Motzkin","year":"1967","unstructured":"Motzkin, T.S.: The arithmetic-geometric inequality. In: Shisha, O. (ed.) Inequalities, Academic Press, London (1967)"},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"P.A. Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Mathematical Programming\u00a096, 293\u2013320 (2003)","journal-title":"Mathematical Programming"},{"key":"9_CR27","doi-asserted-by":"crossref","first-page":"89","DOI":"10.4064\/aa-19-1-89-104","volume":"19","author":"Y. Pourchet","year":"1971","unstructured":"Pourchet, Y.: Sur la r\u00e9presentation en somme de carr\u00e9s des polyn\u00f4mes a une indetermin\u00e9e sur un corps de nombres alg\u00e9braiques. Acta Arithmetica\u00a019, 89\u2013109 (1971)","journal-title":"Acta Arithmetica"},{"key":"9_CR28","series-title":"Springer monographs in mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04648-7","volume-title":"Positive Polynomials: From Hilbert\u2019s 17th Problem to Real Algebra","author":"A. Prestel","year":"2001","unstructured":"Prestel, A., Dalzell, C.N.: Positive Polynomials: From Hilbert\u2019s 17th Problem to Real Algebra. Springer monographs in mathematics. Springer, Heidelberg (2001)"},{"key":"9_CR29","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1137\/1035044","volume":"35","author":"R.T. Rockafellar","year":"1993","unstructured":"Rockafellar, R.T.: Lagrange multipliers and optimality. SIAM review\u00a035, 183\u2013283 (1993)","journal-title":"SIAM review"},{"key":"9_CR30","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":"9_CR31","unstructured":"Strang, G.: Linear Algebra and its Applications, 3rd edn. Brooks\/Cole (1988)"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951), Previous version published as a technical report by the RAND Corporation, J.C.C. McKinsey (1948) (reprinted in [7], pp. 24\u201384)","DOI":"10.1525\/9780520348097"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/11538363_18","volume-title":"Computer Science Logic","author":"A. Tiwari","year":"2005","unstructured":"Tiwari, A.: An algebraic approach to the satisfiability of nonlinear constraints. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 248\u2013262. Springer, Heidelberg (2005)"},{"key":"9_CR34","unstructured":"Weil, A.: Number Theory: An approach through history from Hammurapi to Legendre. Birkh\u00e4user, Basel (1983)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,22]],"date-time":"2021-08-22T05:08:25Z","timestamp":1629608905000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}