{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:19:57Z","timestamp":1743005997232,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_19","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T09:47:55Z","timestamp":1312796875000},"page":"249-264","source":"Crossref","is-referenced-by-count":14,"title":["On the Generation of Positivstellensatz Witnesses in Degenerate Cases"],"prefix":"10.1007","author":[{"given":"David","family":"Monniaux","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Corbineau","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","first-page":"13","volume-title":"ISSAC 2005","author":"J. Adams","year":"2005","unstructured":"Adams, J., Saunders, B.D., Wan, Z.: Signature of symmetric rational matrices and the unitary dual of Lie groups. In: ISSAC 2005, pp. 13\u201320. ACM, New York (2005)"},{"issue":"6","key":"19_CR2","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1145\/235809.235813","volume":"43","author":"S. Basu","year":"1996","unstructured":"Basu, S., Pollack, R., Roy, M.-F.: On the combinatorial and algebraic complexity of quantifier elimination. Journal of the ACM (JACM)\u00a043(6), 1002\u20131045 (1996)","journal-title":"Journal of the ACM (JACM)"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Benson, S.J., Ye, Y.: DSDP5 user guide \u2014 software for semidefinite programming. technical memorandum 277. Argonne National Laboratory (2005)","DOI":"10.2172\/947970"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Benson, S.J., Ye, Y.: Algorithm 875: DSDP5\u2014software for semidefinite programming. ACM Transactions on Mathematical Software 34(3), 16:1\u201316:20 (2008)","DOI":"10.1145\/1356052.1356057"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-74464-1_4","volume-title":"Types for Proofs and Programs","author":"F. Besson","year":"2007","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 48\u201362. Springer, Heidelberg (2007)"},{"key":"19_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization.","author":"S. Boyd","year":"2004","unstructured":"Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004), http:\/\/www.stanford.edu\/~boyd\/cvxbook\/"},{"key":"19_CR7","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":"19_CR8","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition \u2014 twenty years of progress. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 8\u201323 (1998)","DOI":"10.1007\/978-3-7091-9459-1_2"},{"issue":"3","key":"19_CR9","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/S0168-0072(01)00026-4","volume":"111","author":"M. Coste","year":"2001","unstructured":"Coste, M., Lombardi, H., Roy, M.F.: Dynamical method in algebra: effective Nullstellens\u00e4tze. Annals of Pure and Applied Logic\u00a0111(3), 203\u2013256 (2001); Proceedings of the International Conference \u201cAnalyse & Logique\u201d Mons, Belgium, August 25-29 (1997)","journal-title":"Annals of Pure and Applied Logic"},{"key":"19_CR10","unstructured":"Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Tech. Rep. SRI-CSL-06-01, SRI International (May 2006)"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 102\u2013118. Springer, Heidelberg (2007)"},{"key":"19_CR12","unstructured":"INRIA: The Coq Proof Assistant Reference Manual, 8.1 edn. (2006)"},{"key":"19_CR13","first-page":"155","volume-title":"ISSAC (International Symposium on Symbolic and Algebraic Computation)","author":"E. Kaltofen","year":"2008","unstructured":"Kaltofen, E., Li, B., Yang, Z., Zhi, L.: Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars. In: ISSAC (International Symposium on Symbolic and Algebraic Computation), pp. 155\u2013163. ACM, New York (2008)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Kaltofen, E., Li, B., Yang, Z., Zhi, L.: Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients (2009), accepted at J. Symbolic Computation","DOI":"10.1007\/978-3-211-99314-9_9"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"de\u00a0Klerk, E., Pasechnik, D.V.: Products of positive forms, linear matrix inequalities, and Hilbert 17th problem for ternary forms. European Journal of Operational Research, 39\u201345 (2004)","DOI":"10.1016\/j.ejor.2003.08.014"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BF02807438","volume":"12","author":"J.L. Krivine","year":"1964","unstructured":"Krivine, J.L.: Anneaux pr\u00e9ordonn\u00e9s. J. Analyse Math.\u00a012, 307\u2013326 (1964), http:\/\/hal.archives-ouvertes.fr\/hal-00165658\/en\/","journal-title":"J. Analyse Math."},{"key":"19_CR17","volume-title":"Decision Procedures","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008)"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Lombardi, H.: Th\u00e9or\u00e8me des z\u00e9ros r\u00e9els effectif et variantes. Tech. rep., Universit\u00e9 de Franche-Comt\u00e9, Besan con, France (1990), http:\/\/hlombardi.free.fr\/publis\/ThZerMaj.pdf","DOI":"10.5802\/pmb.a-60"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Lombardi, H.: Une borne sur les degr\u00e9s pour le th\u00e9or\u00e8me des z\u00e9ros r\u00e9el effectif. In: Coste, M., Mah\u00e9, L., Roy, M.F. (eds.) Real Algebraic Geometry: Proceedings of the Conference held in Rennes, France. Lecture Notes in Mathematics, vol.\u00a01524, Springer, Heidelberg (1992)","DOI":"10.1007\/BFb0084631"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Mahboubi, A.: Implementing the CAD algorithm inside the Coq system. Mathematical Structures in Computer Sciences\u00a017(1) (2007)","DOI":"10.1017\/S096012950600586X"},{"key":"19_CR21","unstructured":"Parrilo, P.: Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. Ph.D. thesis, California Institute of Technology (2000)"},{"issue":"2","key":"19_CR22","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.tcs.2008.09.025","volume":"409","author":"H. Peyrl","year":"2008","unstructured":"Peyrl, H., Parrilo, P.A.: Computing sum of squares decompositions with rational coefficients. Theoretical Computer Science\u00a0409(2), 269\u2013281 (2008)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"19_CR23","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1215\/S0012-7094-78-04519-2","volume":"45","author":"B. Reznick","year":"1978","unstructured":"Reznick, B.: Extremal PSD forms with few terms. Duke Mathematical Journal\u00a045(2), 363\u2013374 (1978)","journal-title":"Duke Mathematical Journal"},{"key":"19_CR24","volume-title":"Real Algebraic Geometry and Ordered Structures, Contemporary Mathematics","author":"B. Reznick","year":"2000","unstructured":"Reznick, B.: Some concrete aspects of Hilbert\u2019s 17th problem. In: Delzell, C.N., Madden, J.J. (eds.) Real Algebraic Geometry and Ordered Structures, Contemporary Mathematics, vol.\u00a0253. American Mathematical Society, Providence (2000)"},{"key":"19_CR25","first-page":"71","volume-title":"ISSAC (International Symposium on Symbolic and Algebraic Computation)","author":"M. Safey El Din","year":"2008","unstructured":"Safey El Din, M.: Computing the global optimum of a multivariate polynomial over the reals. In: ISSAC (International Symposium on Symbolic and Algebraic Computation), pp. 71\u201378. ACM, New York (2008)"},{"issue":"4","key":"19_CR26","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1016\/j.jco.2004.01.005","volume":"20","author":"M. Schweighofer","year":"2004","unstructured":"Schweighofer, M.: On the complexity of Schm\u00fcdgen\u2019s Positivstellensatz. Journal of Complexity\u00a020(4), 529\u2013543 (2004)","journal-title":"Journal of Complexity"},{"issue":"2","key":"19_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(2), 365\u2013374 (1954), http:\/\/www.jstor.org\/stable\/1969640","journal-title":"Annals of Mathematics"},{"key":"19_CR28","volume-title":"Modular forms, a computational approach. Graduate studies in mathematics","author":"W.A. Stein","year":"2007","unstructured":"Stein, W.A.: Modular forms, a computational approach. Graduate studies in mathematics. American Mathematical Society, Providence (2007)"},{"issue":"207","key":"19_CR29","first-page":"87","volume":"2","author":"G. Stengle","year":"1973","unstructured":"Stengle, G.: A Nullstellensatz and a Positivstellensatz in semialgebraic geometry. Mathematische Annalen\u00a02(207), 87\u201387 (1973)","journal-title":"Mathematische Annalen"},{"key":"19_CR30","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951)"},{"key":"19_CR31","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 for the unsatisfiability of nonlinear constraints. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 248\u2013262. Springer, Heidelberg (2005)"},{"issue":"1","key":"19_CR32","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1137\/1038003","volume":"38","author":"L. Vandenberghe","year":"1996","unstructured":"Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Review\u00a038(1), 49\u201395 (1996)","journal-title":"SIAM Review"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,30]],"date-time":"2021-11-30T00:15:52Z","timestamp":1638231352000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}