{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:48:54Z","timestamp":1725558534753},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141270"},{"type":"electronic","value":"9783642141287"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_17","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T06:45:36Z","timestamp":1277793936000},"page":"189-203","source":"Crossref","is-referenced-by-count":5,"title":["A Formal Quantifier Elimination for Algebraically Closed Fields"],"prefix":"10.1007","author":[{"given":"Cyril","family":"Cohen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Barras, B.: Sets in coq, coq in sets. In: Proceedings of the 1st Coq Workshop. Technical University of Munich Research Report (2009)"},{"key":"17_CR2","series-title":"Algorithms and Computation in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry","author":"S. Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry, Algorithms and Computation in Mathematics. Springer, New York (2006)"},{"issue":"1-3","key":"17_CR3","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.apal.2004.01.002","volume":"129","author":"S. Berardi","year":"2004","unstructured":"Berardi, S., Valentini, S.: Krivine\u2019s intuitionistic proof of classical completeness for countable languages. Ann. Pure Appl. Logic\u00a0129(1-3), 93\u2013106 (2004)","journal-title":"Ann. Pure Appl. Logic"},{"key":"17_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art: the Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: the Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"key":"17_CR6","first-page":"265","volume-title":"The Concise Handbook of Algebra","author":"B. Buchberger","year":"2002","unstructured":"Buchberger, B.: Groebner Bases: Applications. In: Mikhalev, A.V., Pilz, G.F. (eds.) The Concise Handbook of Algebra, pp. 265\u2013268. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"17_CR7","unstructured":"Chevalley, C., Cartan, H.: Sch\u00e9mas normaux; morphismes; ensembles constructibles. In: S\u00e9minaire Henri Cartan, Numdam, vol.\u00a08, pp. 1\u201310 (1955-1956), http:\/\/www.numdam.org\/item?id=SHC_1955-1956__8__A7_0"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"TPHOLs 2009","author":"F. Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009)"},{"issue":"4","key":"17_CR9","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1006\/jsco.2002.0552","volume":"34","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. Journal of Symbolic Computation\u00a034(4), 271\u2013286 (2002)","journal-title":"Journal of Symbolic Computation"},{"key":"#cr-split#-17_CR10.1","unstructured":"Harrison, J.: Complex quantifier elimination in HOL. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001: Supplemental Proceedings, Division of Informatics, University of Edinburgh, pp. 159???174 (2001);"},{"key":"#cr-split#-17_CR10.2","unstructured":"Published as Informatics Report Series EDI-INF-RR-0046, http:\/\/www.informatics.ed.ac.uk\/publications\/report\/0046.html"},{"key":"17_CR11","volume-title":"A shorter model theory","author":"W. Hodges","year":"1997","unstructured":"Hodges, W.: A shorter model theory. Cambridge University Press, Cambridge (1997)"},{"key":"17_CR12","unstructured":"G\u00f6del, K.: \u00dcber die Vollst\u00e4ndigkeit des Logikkalk\u00fcls. PhD thesis, University of Vienna, Austria (1929)"},{"key":"17_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-71070-7_3","volume-title":"Automated Reasoning","author":"T. Nipkow","year":"2008","unstructured":"Nipkow, T.: Linear quantifier elimination. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 18\u201333. Springer, Heidelberg (2008)"},{"key":"17_CR14","unstructured":"O\u2019Connor, R.: Incompleteness & Completeness, Formalizing Logic and Analysis in Type Theory. PhD thesis, Radboud University Nijmegen, Netherlands (2009)"},{"key":"17_CR15","unstructured":"Pottier, L.: Connecting gr\u00f6bner bases programs with coq to do proofs in algebra, geometry and arithmetics. In: LPAR Workshops. CEUR Workshop Proceedings, vol.\u00a0418. CEUR-WS.org (2008)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/11541868_19","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Ridge","year":"2005","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 294\u2013309. Springer, Heidelberg (2005)"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J. Robinson","year":"1949","unstructured":"Robinson, J.: Definability and decision problems in arithmetic. Journal of Symbolic Logic\u00a014, 98\u2013114 (1949)","journal-title":"Journal of Symbolic Logic"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Simpson, C.T.: Formalized proof, computation, and the construction problem in algebraic geometry (2004)","DOI":"10.1007\/0-306-48658-X_9"},{"key":"17_CR19","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. In: RAND Corp., Santa Monica, CA (1948) (manuscript); Republished as A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,1]],"date-time":"2023-06-01T15:51:22Z","timestamp":1685634682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}