{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T00:31:13Z","timestamp":1769819473633,"version":"3.49.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319213613","type":"print"},{"value":"9783319213620","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-21362-0_5","type":"book-chapter","created":{"date-parts":[[2015,7,17]],"date-time":"2015-07-17T01:56:52Z","timestamp":1437098212000},"page":"72-93","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems"],"prefix":"10.1007","author":[{"given":"Vesna","family":"Marinkovi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Predrag","family":"Jani\u010di\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Schreck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,18]]},"reference":[{"issue":"3","key":"5_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0010-4485(88)90019-X","volume":"20","author":"B Aldefeld","year":"1988","unstructured":"Aldefeld, B.: Variations of geometries based on a geometric-reasoning method. Comput. Aided Des. 20(3), 117\u2013126 (1988)","journal-title":"Comput. Aided Des."},{"key":"5_CR2","unstructured":"Boutry, P., Narboux, J., Schreck, P., Braun, G.: Using small scale automation to improve both accessibility and readability of formal proofs in geometry. In: Proceedings of the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), CISUC TR2014\/02, Universidade de Coimbra (2014)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-40672-0_7","volume-title":"Automated Deduction in Geometry","author":"G Braun","year":"2013","unstructured":"Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) ADG 2012. LNCS, vol. 7993, pp. 89\u2013109. Springer, Heidelberg (2013)"},{"key":"5_CR4","first-page":"487","volume":"27","author":"W Buoma","year":"1995","unstructured":"Buoma, W., Fudos, I., Hoffman, C., Cai, J., Paige, R.: A geometric constraint solver. CAD 27, 487\u2013501 (1995)","journal-title":"CAD"},{"issue":"4","key":"5_CR5","first-page":"353","volume":"3","author":"M Buthion","year":"1979","unstructured":"Buthion, M.: Un programme qui r\u00e9soud formellement des probl\u00e8mes de constructions g\u00e9om\u00e9triques. RAIRO Informatique 3(4), 353\u2013387 (1979)","journal-title":"RAIRO Informatique"},{"key":"5_CR6","unstructured":"Chen, G.: Les constructions \u00e0 la r\u00e8gle et au compas par une m\u00e9thode alg\u00e9brique. Technical report Rapport de DEA, Universit\u00e9 Louis Pasteur (1992)"},{"issue":"2","key":"5_CR7","first-page":"69","volume":"23","author":"M Djori\u0107","year":"2004","unstructured":"Djori\u0107, M., Jani\u010di\u0107, P.: Constructions, instructions, interactions. Teach. Mathe. Appl. 23(2), 69\u201388 (2004)","journal-title":"Teach. Mathe. Appl."},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0004-3702(97)00070-2","volume":"99","author":"J-F Dufourd","year":"1998","unstructured":"Dufourd, J.-F., Mathis, P., Schreck, P.: Geometric construction by assembling solved subfigures. Artif. Intell. J. 99(1), 73\u2013119 (1998)","journal-title":"Artif. Intell. J."},{"issue":"1","key":"5_CR9","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0004-3702(00)00061-8","volume":"124","author":"C Essert-Villard","year":"2000","unstructured":"Essert-Villard, C., Schreck, P., Dufourd, J.-F.: Sketch-based pruning of a solution space within a formal geometric constraint solver. Artif. Intell. 124(1), 139\u2013159 (2000)","journal-title":"Artif. Intell."},{"issue":"2","key":"5_CR10","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/S0010-4485(97)00055-9","volume":"30","author":"X-S Gao","year":"1998","unstructured":"Gao, X.-S., Chou, S.-C.: Solving geometric constraint systems. ii. A symbolic approach and decision of rc-constructibility. Comput. Aided Des. 30(2), 115\u2013122 (1998)","journal-title":"Comput. Aided Des."},{"key":"5_CR11","unstructured":"Gelernter, H.: Realization of a geometry theorem proving machine. In: Proceedings of the International Conference Information Processing, Paris, pp. 273\u2013282, 15\u201320 June 1959"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-25379-9_8","volume-title":"Certified Programs and Proofs","author":"J-D G\u00e9nevaux","year":"2011","unstructured":"G\u00e9nevaux, J.-D., Narboux, J., Schreck, P.: Formalization of Wu\u2019s simple method in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 71\u201386. Springer, Heidelberg (2011)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-21046-4_3","volume-title":"Automated Deduction in Geometry","author":"B Gr\u00e9goire","year":"2011","unstructured":"Gr\u00e9goire, B., Pottier, L., Th\u00e9ry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS, vol. 6301, pp. 42\u201359. Springer, Heidelberg (2011)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Korthikanti, V.A., Tiwari, A.: Synthesizing geometry constructions. In: Programming Language Design and Implementation, PLDI 2011, pp. 50\u201361. ACM (2011)","DOI":"10.1145\/1993316.1993505"},{"issue":"1\u20132","key":"5_CR15","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10817-009-9135-8","volume":"44","author":"P Jani\u010di\u0107","year":"2010","unstructured":"Jani\u010di\u0107, P.: Geometry constructions language. J. Autom. Reasoning 44(1\u20132), 3\u201324 (2010)","journal-title":"J. Autom. Reasoning"},{"issue":"5\u20136","key":"5_CR16","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1142\/S0218195906002105","volume":"16","author":"C Jermann","year":"2006","unstructured":"Jermann, C., Trombettoni, G., Neveu, B., Mathis, P.: Decomposition of geometric constraint systems: a survey. Int. J. Comput. Geom. Appl. 16(5\u20136), 379\u2013414 (2006). CNRS MathSTIC","journal-title":"Int. J. Comput. Geom. Appl."},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0022-0000(85)90013-3","volume":"30","author":"S Landau","year":"1985","unstructured":"Landau, S., Miller, G.L.: Solvability by radicals is in polynomial time. J. Comput. Syst. Sci. 30(2), 179\u2013208 (1985)","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR18","unstructured":"Lebesgue, H.: Le\u00e7ons sur les constructions g\u00e9om\u00e9triques. Gauthier-Villars, Paris (1950) (in French), re-edition by Editions Jacques Gabay, France"},{"key":"5_CR19","unstructured":"Lemaire, F., Moreno-Maza, M., Xie, Y.: The RegularChains library in Maple 10. In: Kotsireas, I.S. (ed.) Proceedings of Maple Summer Conference 2005, Waterloo, Canada, pp. 355\u2013368 (2005)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Mari\u0107, F., Petrovi\u0107, I., Petrovi\u0107, D., Jani\u010di\u0107, P.: Formalization and implementation of algebraic methods in geometry. In: Quaresma, P., Back, R.-J. (eds.) Proceedings of First Workshop on CTP Components for Educational Software, Wroc\u0142aw, Poland, 31 July 2011. Electronic Proceedings in Theoretical Computer Science, vol. 79, pp. 63\u201381. Open Publishing Association (2012)","DOI":"10.4204\/EPTCS.79.4"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-31374-5_9","volume-title":"Intelligent Computer Mathematics","author":"V Marinkovi\u0107","year":"2012","unstructured":"Marinkovi\u0107, V., Jani\u010di\u0107, P.: Towards understanding triangle construction problems. In: Campbell, J.A., Jeuring, J., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 127\u2013142. Springer, Heidelberg (2012)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-45949-9_1","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL. LNCS, vol. 2283, p. 3. Springer, Heidelberg (2002)"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Owen, J.: Algebraic solution for geometry from dimensional constraints. In: Proceedings of the 1th ACM Symposium of Solid Modeling and CAD\/CAM Applications, pp. 397\u2013407. ACM Press (1991)","DOI":"10.1145\/112515.112573"},{"issue":"2","key":"5_CR24","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0004-3702(74)90028-9","volume":"5","author":"JM Scandura","year":"1974","unstructured":"Scandura, J.M., Durnin, J.H., Wulfeck II, W.H.: Higher order rule characterization of heuristics for compass and straight edge constructions in geometry. Artif. Intell. 5(2), 149\u2013183 (1974)","journal-title":"Artif. Intell."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Schreck, P.: Robustness in CAD Geometric Constructions. In: IV 2001, pp. 111\u2013116 (2001)","DOI":"10.1109\/IV.2001.942046"},{"issue":"3","key":"5_CR26","first-page":"223","volume":"8","author":"P Schreck","year":"1994","unstructured":"Schreck, P.: Mod\u00e9lisation et implantation d\u2019un syst\u00e8me \u00e0 base de connaissances pour les constructions g\u00e9om\u00e9triques. Revue d\u2019Intelligence Artificielle 8(3), 223\u2013247 (1994)","journal-title":"Revue d\u2019Intelligence Artificielle"},{"key":"5_CR27","unstructured":"Schreck, P., Mathis, P.: Rc-constructibility of problems in Wernick\u2019s and Connelly\u2019s lists. In: Proceedings of the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), CISUC TR2014\/02, Universidade de Coimbra (2014)"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-25070-5_12","volume-title":"Automated Deduction in Geometry","author":"S Stojanovi\u0107","year":"2011","unstructured":"Stojanovi\u0107, S., Pavlovi\u0107, V., Jani\u010di\u0107, P.: A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS, vol. 6877, pp. 201\u2013220. Springer, Heidelberg (2011)"},{"issue":"4","key":"5_CR29","doi-asserted-by":"publisher","first-page":"227","DOI":"10.2307\/2690164","volume":"55","author":"W Wernick","year":"1982","unstructured":"Wernick, W.: Triangle constructions vith three located points. Math. Mag. 55(4), 227\u2013230 (1982)","journal-title":"Math. Mag."},{"issue":"1","key":"5_CR30","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.jal.2007.02.001","volume":"6","author":"V Pambuccian","year":"2008","unstructured":"Pambuccian, V.: Axiomatizing geometric constructions. J. Appl. Logic 6(1), 24\u201346 (2008)","journal-title":"J. Appl. Logic"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-30870-3_6","volume-title":"How the World Computes","author":"M Beeson","year":"2012","unstructured":"Beeson, M.: Logic of ruler and compass constructions. In: Cooper, S.B., Dawar, A., L\u00f6we, B. (eds.) CiE 2012. LNCS, vol. 7318, pp. 46\u201355. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Geometry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21362-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T09:20:14Z","timestamp":1748510414000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21362-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319213613","9783319213620"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21362-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"18 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}