{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:04:16Z","timestamp":1746745456732},"reference-count":32,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2007,2,1]],"date-time":"2007-02-01T00:00:00Z","timestamp":1170288000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2007,2]]},"abstract":"<jats:p>The Coq system is a Curry\u2013Howard based proof assistant. Therefore, it contains a full functional, strongly typed programming language, which can be used to enhance the system with powerful automation tools through the implementation of reflexive tactics. We present the implementation of a cylindrical algebraic decomposition algorithm within the Coq system, whose certification leads to a proof producing decision procedure for the first-order theory of real numbers.<\/jats:p>","DOI":"10.1017\/s096012950600586x","type":"journal-article","created":{"date-parts":[[2007,3,7]],"date-time":"2007-03-07T10:59:58Z","timestamp":1173265198000},"page":"99-127","source":"Crossref","is-referenced-by-count":16,"title":["Implementing the cylindrical algebraic decomposition within the Coq system"],"prefix":"10.1017","volume":"17","author":[{"given":"ASSIA","family":"MAHBOUBI","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2007,2,1]]},"reference":[{"key":"S096012950600586X_rf30","unstructured":"The Coq Development Team (2004) The Coq Proof Assistant Reference Manual Version 8.0, Institut National de Recherche en Informatique et en Automatique. (Available at http:\/\/coq.inria.fr\/)"},{"key":"S096012950600586X_rf26","doi-asserted-by":"publisher","DOI":"10.1002\/1521-3870(200202)48:2<297::AID-MALQ297>3.0.CO;2-G"},{"key":"S096012950600586X_rf22","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_37"},{"key":"S096012950600586X_rf21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61497-2"},{"key":"S096012950600586X_rf32","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00639-4"},{"key":"S096012950600586X_rf27","first-page":"98","volume-title":"TYPES 2004","author":"Sacerdoti","year":"2006"},{"key":"S096012950600586X_rf19","unstructured":"Gr\u00e9goire B. and Th\u00e9ry L. (2006) Certifying Large Prime Numbers: a purely functional library for modular arithmetic To appear in Proceedings of IJCAR06. (Available at http:\/\/gforge.inria\/projects\/coqprime\/)"},{"key":"S096012950600586X_rf18","first-page":"98","volume-title":"Proceedings of the TPHOLs 2005","author":"Gr\u00e9goire","year":"2005"},{"key":"S096012950600586X_rf15","doi-asserted-by":"publisher","DOI":"10.1145\/261320.261324"},{"key":"S096012950600586X_rf14","first-page":"111","volume-title":"Proceedings of the ISSAC 2004","author":"Dolzmann","year":"2004"},{"key":"S096012950600586X_rf13","volume-title":"Proceedings of Calculemus 2005","author":"Delahaye","year":"2005"},{"key":"S096012950600586X_rf12","volume-title":"Proceedings of Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark)","author":"Delahaye","year":"2002"},{"key":"S096012950600586X_rf10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-07407-4_17"},{"key":"S096012950600586X_rf7","doi-asserted-by":"crossref","unstructured":"Brown C. W. (2004) QEPCAD. (Homepage: http:\/\/www.cs.usna.edu\/~qepcad\/B\/QEPCAD.html)","DOI":"10.1145\/980175.980185"},{"key":"S096012950600586X_rf4","doi-asserted-by":"crossref","unstructured":"Basu S. , Pollack R. and Roy M. (2003) Algorithms in Real Algebraic Geometry. Algorithms and Computation in Mathematics 10, Springer-Verlag. (Draft of the second version available at http:\/\/name.math.univ-rennes1.fr\/marie-francoise.roy\/bpr-posted1.html.)","DOI":"10.1007\/978-3-662-05355-3"},{"key":"S096012950600586X_rf3","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004501"},{"key":"S096012950600586X_rf2","unstructured":"Avigad J. , Donnelly K. , Gray D. and Raff P. (2005) A Formally Verified Proof of the Prime Number Theorem. To appear in the ACM Transactions on Computational Logic. (Available at http:\/\/arxiv.org\/abs\/cs.AI\/0509025.)"},{"key":"S096012950600586X_rf1","volume-title":"Proceedings of the 5th Symposium on Logic in Computer Science (LICS)","author":"Allen","year":"1990"},{"key":"S096012950600586X_rf16","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006031329384"},{"key":"S096012950600586X_rf20","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006023127567"},{"key":"S096012950600586X_rf24","first-page":"295","volume-title":"CADE","author":"McLaughlin","year":"2005"},{"key":"S096012950600586X_rf6","unstructured":"Bronstein M. (2004) AXIOM \u2013 The Scientific Computation System. (Homepage: http:\/\/axiom.axiom-developer.org\/axiom-website\/community.html)"},{"key":"S096012950600586X_rf31","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026518331905"},{"key":"S096012950600586X_rf28","unstructured":"Strzebonski A. (2004) Cylindrical Algebraic Decomposition. In: MathWorld \u2013 A Wolfram Web Resource, created by Eric W. Weisstein. (Available at http:\/\/mathworld.wolfram.com\/CylindricalAlgebraicDecomposition.html)"},{"key":"S096012950600586X_rf25","first-page":"309","volume-title":"TYPES 2003","author":"Niqui","year":"2003"},{"key":"S096012950600586X_rf17","first-page":"235","volume-title":"International Conference on Functional Programming 2002","author":"Gr\u00e9goire","year":"2002"},{"key":"S096012950600586X_rf5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S096012950600586X_rf8","doi-asserted-by":"publisher","DOI":"10.1145\/968708.968710"},{"key":"S096012950600586X_rf11","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80152-6"},{"key":"S096012950600586X_rf29","unstructured":"Tarski A. (1948) A Decision Method for Elementary Algebra and Geometry, The RAND Corporation, Santa Monica, U.S. Air Force Project RAND, R-109."},{"key":"S096012950600586X_rf23","volume-title":"Journ\u00e9es Fran\u00e7aises des Languages Applicatifs","author":"Mahboubi","year":"2002"},{"key":"S096012950600586X_rf9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-9459-1"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012950600586X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T21:55:22Z","timestamp":1683755722000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012950600586X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,2]]}},"alternative-id":["S096012950600586X"],"URL":"https:\/\/doi.org\/10.1017\/s096012950600586x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2]]}}}