{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T10:02:40Z","timestamp":1771063360798,"version":"3.50.1"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2014,11,12]],"date-time":"2014-11-12T00:00:00Z","timestamp":1415750400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10472-014-9436-4","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T21:08:44Z","timestamp":1415999324000},"page":"271-308","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formalizing complex plane geometry"],"prefix":"10.1007","volume":"74","author":[{"given":"Filip","family":"Mari\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Danijela","family":"Petrovi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,11,12]]},"reference":[{"issue":"2","key":"9436_CR1","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G Barthe","year":"2003","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261\u2013293 (2003)","journal-title":"J. Funct. Program."},{"key":"9436_CR2","doi-asserted-by":"crossref","unstructured":"Cohen, C.: Pragmatic quotient types in Coq. In: Sandrine, B., Christine, P.-M., Pichardie, D. (eds.) Interactive Theorem Proving, vol. 7998 of Lecture Notes in Computer Science, pp 213\u2013228. Springer Berlin Heidelberg (2013)","DOI":"10.1007\/978-3-642-39634-2_17"},{"key":"9436_CR3","doi-asserted-by":"crossref","unstructured":"Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-Order Intuitionistic Formalization and Proofs in Hilberts Elementary Geometry. In: Automated Deduction in Geometry, vol. 2061 of Lecture Notes in Computer Science. Springer (2001)","DOI":"10.1007\/3-540-45410-1_17"},{"key":"9436_CR4","unstructured":"Duprat, J.: Constructors: a ruler and a pair of compasses TYPES 2002 (2002)"},{"key":"9436_CR5","doi-asserted-by":"crossref","unstructured":"G\u00e9nevaux, J.-D., Narboux, J., Schreck, P.: Formalization of Wu\u2019s simple method in Coq. In: CPP, vol. 7086 of Lecture Notes in Computer Science. Springer (2011)","DOI":"10.1007\/978-3-642-25379-9_8"},{"key":"9436_CR6","doi-asserted-by":"crossref","unstructured":"Geuvers, H., Wiedijk, F., Zwanenburg, J.: A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. In: Types for Proofs and Programs, vol. 2277 of Lecture Notes in Computer Science. Springer (2002)","DOI":"10.1007\/3-540-45842-5_7"},{"key":"9436_CR7","unstructured":"Gr\u00e9goire, B., Pottier, L., Th\u00e9ry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Automated Deduction in Geometry, vol. 6301 of Lecture Notes in Computer Science. Springer (2008)"},{"key":"9436_CR8","doi-asserted-by":"crossref","unstructured":"Guilhot, F.: Formalisation en coq et visualisation d\u2019un cours de g\u00e9om\u00e9trie pour le lyc\u00e9e. Tech. et Sci. Informatiques 24(9) (2005)","DOI":"10.3166\/tsi.24.1113-1138"},{"key":"9436_CR9","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in isabelle. In: Types for Proofs and Programs, vol. 4502 of Lecture Notes in Computer Science, pp 160\u2013174. Springer Berlin Heidelberg (2007)","DOI":"10.1007\/978-3-540-74464-1_11"},{"key":"9436_CR10","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A HOL Theory of Euclidean Space. In: TPHOLs, vol. 3603 of Lecture Notes in Computer Science. Springer (2005)","DOI":"10.1007\/11541868_8"},{"key":"9436_CR11","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Without loss of generality.. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009, vol. 5674 of LNCS, Munich. Springer-Verlag, Germany (2009)","DOI":"10.1007\/978-3-642-03359-9_3"},{"key":"9436_CR12","doi-asserted-by":"crossref","unstructured":"Harrison, J.: The HOL light theory of euclidean space. J. Autom. Reason. 50(2) (2013)","DOI":"10.1007\/s10817-012-9250-9"},{"key":"9436_CR13","unstructured":"Hilbert, D., Townsend, E.J.: The Foundations Of Geometry. Kessinger Publishing (2006)"},{"key":"9436_CR14","unstructured":"Hille, E.: Analytic Function Theory. AMS Chelsea Publishing. American Mathematical Society (1973)"},{"key":"9436_CR15","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and Transfer A Modular Design for Quotients in Isabelle\/HOL Certified Programs and Proofs, vol. 8307 of LNCS. Springer International Publishing (2013)","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"9436_CR16","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P., Narboux, J., Quaresma, P.: The area method. J. Autom. Reason. 48(4) (2012)","DOI":"10.1007\/s10817-010-9209-7"},{"key":"9436_CR17","unstructured":"Kahn, G.: Constructive geometry according to Jan von Plato. Coq contribution, Coq V5.10 (1995)"},{"key":"9436_CR18","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, C.: Quotients revisited for Isabelle\/HOL. In: Proceedings of the 2011 ACM Symposium on Applied Computing, SAC \u201911, pp 1639\u20131644, New York, NY USA ACM (2011)","DOI":"10.1145\/1982185.1982529"},{"key":"9436_CR19","doi-asserted-by":"crossref","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing Projective Plane geometry in Coq. In: Automated Deduction in Geometry, vol. 6301 of Lecture Notes in Computer Science. Springer (2011)","DOI":"10.1007\/978-3-642-21046-4_7"},{"key":"9436_CR20","unstructured":"McKenzie Makarios, T.J.: A mechanical verification of the independence of Tarski\u2019s Euclidean axiom Master\u2019s thesis. Victoria University of Wellington (2012)"},{"key":"9436_CR21","unstructured":"Mari\u0107, F., Petrovi\u0107, D.: Formalizing analytic geometries , Automated Deduction in Geometry (2012)"},{"key":"9436_CR22","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: THedu, vol. 79 of EPTCS (2011)","DOI":"10.4204\/EPTCS.79.4"},{"key":"9436_CR23","doi-asserted-by":"crossref","unstructured":"Meikle, L., Fleuriot, J.: Formalizing Hilberts Grundlagen in Isabelle\/Isar. In: Theorem Proving in Higher Order Logics, vol. 2758 of Lecture Notes in Computer Science. Springer (2003)","DOI":"10.1007\/10930755_21"},{"key":"9436_CR24","unstructured":"Milewski, R.: Fundamental theorem of algebra. Formalized Mathematics 9(3) (2001)"},{"key":"9436_CR25","doi-asserted-by":"crossref","unstructured":"Narboux, J.: Mechanical Theorem Proving in Tarski\u2019s Geometry. In: Automated Deduction in Geometry, vol. 4869 of Lecture Notes in Computer Science. Springer (2007)","DOI":"10.1007\/978-3-540-77356-6_9"},{"key":"9436_CR26","doi-asserted-by":"crossref","unstructured":"Needham, T.: Visual Complex Analysis. Oxford University Press (1998)","DOI":"10.1093\/oso\/9780198534471.001.0001"},{"key":"9436_CR27","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Lawrence, C.P., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic vol. 2283 of LNCS. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9436_CR28","doi-asserted-by":"crossref","unstructured":"Penrose, R., Rindler, W.: Spinors and Space-Time Cambridge Monographs on Mathematical Physics. Cambridge University Press (1987)","DOI":"10.1017\/CBO9780511524486"},{"key":"9436_CR29","doi-asserted-by":"crossref","unstructured":"Schwabh\u00e4user, W., Szmielew, W., Tarski, A., Beeson, M.: Metamathematische Methoden in der Geometrie. Springer Verlag (1983)","DOI":"10.1007\/978-3-642-69418-9"},{"key":"9436_CR30","unstructured":"Schwerdtfeger, H.: Geometry of Complex Numbers Dover Books on Mathematics. Dover Publications (1979)"},{"key":"9436_CR31","unstructured":"Scott, P.: Mechanising Hilberts Foundations of Geometry in Isabelle. University of Edinburgh, Master\u2019s thesis (2008)"},{"key":"9436_CR32","unstructured":"Sternagel, C., Thiemann, R.: Executable matrix operations on matrices of arbitrary dimensions Archive of Formal Proofs (2010). Formal proof development. http:\/\/afp.sf.net\/entries\/Matrix.shtml"},{"key":"9436_CR33","doi-asserted-by":"crossref","unstructured":"von Plato, J.: The axioms of constructive geometry. Ann. Pure Appl. Logic 76(2) (1995)","DOI":"10.1016\/0168-0072(95)00005-2"},{"key":"9436_CR34","unstructured":"Wenzel M.: Isabelle\/Isar \u2014 a generic framework for human-readable proof documents. In: From Insight to Proof \u2014 Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric vol. 10(23) University of Bialystok (2007)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9436-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-014-9436-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9436-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,5]],"date-time":"2024-06-05T01:35:44Z","timestamp":1717551344000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-014-9436-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,12]]},"references-count":34,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["9436"],"URL":"https:\/\/doi.org\/10.1007\/s10472-014-9436-4","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,12]]}}}