{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T14:10:33Z","timestamp":1742998233661,"version":"3.40.3"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031617157"},{"type":"electronic","value":"9783031617164"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-61716-4_3","type":"book-chapter","created":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:47:52Z","timestamp":1716954472000},"page":"36-53","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Safe Smooth Paths Between Straight Line Obstacles"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5052-3019","authenticated-orcid":false,"given":"Yves","family":"Bertot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,22]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Basu, S., Pollack, R., Roy M.F.: Algorithms in Real Algebraic Geometry, volume\u00a010 of Algorithms and Computation in Mathematics, 2nd edn. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/3-540-33099-2","DOI":"10.1007\/3-540-33099-2"},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-02508-3_1","volume-title":"ICTAC 2018","author":"Y Bertot","year":"2018","unstructured":"Bertot, Y.: Formal Verification of a geometry algorithm: a quest for abstract views and symmetry in coq proofs. In: Fischer, B., Uustalu, T. (eds.) ICTAC 2018, vol. 11187, pp. 3\u201310. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-030-02508-3_1"},{"issue":"04","key":"3_CR3","doi-asserted-by":"publisher","first-page":"731","DOI":"10.1017\/S0960129511000090","volume":"21","author":"Y Bertot","year":"2011","unstructured":"Bertot, Y., Guilhot, F., Mahboubi, A.: A formal study of Bernstein coefficients and polynomials. Math. Struct. Comput. Sci. 21(04), 731\u2013761 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"102","key":"3_CR4","first-page":"1","volume":"8","author":"C Cohen","year":"2012","unstructured":"Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods Comput. Sci. 8(102), 1\u201340 (2012)","journal-title":"Logical Methods Comput. Sci."},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"EW Dijkstra","year":"1959","unstructured":"Dijkstra, E.W.: A note on two problems in connexion with graphs. Numer. Math. 1(1), 269\u2013271 (1959)","journal-title":"Numer. Math."},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-14052-5_16","volume-title":"Interactive Theorem Proving","author":"JF Dufourd","year":"2010","unstructured":"Dufourd, J.F., Bertot, Y.: Formal study of plane Delaunay triangulation. In: Paulson, L., Kaufmann, M. (eds.) ITP 2010, vol. 6172, pp. 211\u2013226. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_16"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45842-5_7","volume-title":"TYPES 2000","author":"H Geuvers","year":"2000","unstructured":"Geuvers, H., Wiedijk, F., Zwanenburg, J.: A constructive proof of the fundamental theorem of algebra without using the rationals. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 96\u2013111. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45842-5_7"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Knuth, D.: Axioms and Hulls. Number 606 in Lecture Notes in Computer Science. Springer-Verlag, Heidelberg (1991). DOI: https:\/\/doi.org\/10.1007\/3-540-55611-7","DOI":"10.1007\/3-540-55611-7"},{"key":"3_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4022-9","volume-title":"Robot Motion Planning","author":"J-C Latombe","year":"1991","unstructured":"Latombe, J.-C.: Robot Motion Planning. Kluwer Academic Publishers, Norwell (1991)"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-44755-5_24","volume-title":"TPHOLs 2001","author":"D Pichardie","year":"2001","unstructured":"Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 346\u2013361. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44755-5_24"},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-030-01090-4_5","volume-title":"ATVA 2018","author":"A Rizaldi","year":"2018","unstructured":"Rizaldi, A., Immler, F., Sch\u00fcrmann, B., Althoff, M.: A Formally Verified Motion Planner for Autonomous Vehicles. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 75\u201390. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_5"},{"issue":"2","key":"3_CR12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s10817-013-9299-0","volume":"53","author":"J Zsid\u00f3","year":"2014","unstructured":"Zsid\u00f3, J.: Theorem of Three Circles in Coq. J. Autom. Reason. 53(2), 105\u2013127 (2014)","journal-title":"J. Autom. Reason."}],"container-title":["Lecture Notes in Computer Science","Logics and Type Systems in Theory and Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-61716-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:47:58Z","timestamp":1716954478000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-61716-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031617157","9783031617164"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-61716-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"22 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}