{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,3]],"date-time":"2026-01-03T14:47:12Z","timestamp":1767451632424,"version":"3.37.3"},"reference-count":68,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,4,30]],"date-time":"2020-04-30T00:00:00Z","timestamp":1588204800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,4,30]],"date-time":"2020-04-30T00:00:00Z","timestamp":1588204800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004564","name":"Ministarstvo Prosvete, Nauke i Tehnolo\u0161kog Razvoja","doi-asserted-by":"publisher","award":["174021"],"award-info":[{"award-number":["174021"]}],"id":[{"id":"10.13039\/501100004564","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,1]]},"DOI":"10.1007\/s10817-020-09551-2","type":"journal-article","created":{"date-parts":[[2020,4,30]],"date-time":"2020-04-30T17:04:31Z","timestamp":1588266271000},"page":"31-73","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formalization of the Poincar\u00e9 Disc Model of Hyperbolic Geometry"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3840-9931","authenticated-orcid":false,"given":"Danijela","family":"Simi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Filip","family":"Mari\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Boutry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,30]]},"reference":[{"key":"9551_CR1","unstructured":"Assaf, A.: A framework for defining computational higher-order logics. Theses, \u00c9cole polytechnique (2015)"},{"key":"9551_CR2","doi-asserted-by":"crossref","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: theories and proof contexts. In: Mathematical Knowledge Management, MKM, Proceedings, pp. 31\u201343 (2006)","DOI":"10.1007\/11812289_4"},{"key":"9551_CR3","unstructured":"Beeson, M.: Proving Hilbert\u2019s axioms in Tarski geometry (2014). http:\/\/www.michaelbeeson.com\/research\/papers\/TarskiProvesHilbert.pdf"},{"issue":"11","key":"9551_CR4","doi-asserted-by":"publisher","first-page":"1199","DOI":"10.1016\/j.apal.2015.07.006","volume":"166","author":"M Beeson","year":"2015","unstructured":"Beeson, M.: A constructive version of Tarski\u2019s geometry. Ann. Pure Appl. Log. 166(11), 1199\u20131273 (2015)","journal-title":"Ann. Pure Appl. Log."},{"key":"9551_CR5","unstructured":"Beeson, M., Boutry, P., Braun, G., Gries, C., Narboux, J.: GeoCoq (2018). https:\/\/hal.inria.fr\/hal-01912024\/"},{"issue":"1","key":"9551_CR6","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10817-016-9392-2","volume":"58","author":"M Beeson","year":"2017","unstructured":"Beeson, M., Wos, L.: Finding proofs in Tarskian geometry. J. Autom. Reason. 58(1), 181\u2013207 (2017)","journal-title":"J. Autom. Reason."},{"key":"9551_CR7","unstructured":"Beltrami, E.: Saggio di interpretazione della geometria Non-Euclidea. s.n. (1868)"},{"key":"9551_CR8","unstructured":"Bolyai, J.: Appendix, Scientiam Spatii absolute veram exhibens: a veritate aut falsitate Axiomatis XI. Euclidei (a priori haud unquam decidenda) independentem; adjecta ad casum falsitatis, quadratura circuli geometrica. Auctore Johanne Bolyai de eadem, Geometrarum in Exercitu Caesareo Regio Austriaco Castrensium Capitaneo. Coll. Ref. (1832)"},{"key":"9551_CR9","volume-title":"Foundations of Geometry","author":"K Borsuk","year":"1960","unstructured":"Borsuk, K., Szmielew, W.: Foundations of Geometry. North-Holland, New York (1960)"},{"key":"9551_CR10","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.jsc.2018.04.007","volume":"90","author":"P Boutry","year":"2019","unstructured":"Boutry, P., Braun, G., Narboux, J.: Formalization of the arithmetization of Euclidean plane geometry and applications. J. Symbol. Comput. 90, 149\u2013168 (2019)","journal-title":"J. Symbol. Comput."},{"key":"9551_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-017-9422-8","volume":"62","author":"P Boutry","year":"2019","unstructured":"Boutry, P., Gries, C., Narboux, J., et al.: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. J Autom. Reason. 62, 1\u201368 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9422-8","journal-title":"J Autom. Reason."},{"key":"9551_CR12","unstructured":"Boutry, P., Narboux, J., Schreck, P., Braun, G.: A short note about case distinctions in Tarski\u2019s geometry. In: Botana, F., Quaresma, P. (eds.) Proceedings of the Tenth International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2014, pp. 51\u201365. Coimbra, Portugal (2014)"},{"key":"9551_CR13","first-page":"62","volume":"2016","author":"D Braun","year":"2016","unstructured":"Braun, D., Magaud, N., Schreck, P.: An equivalence proof between rank theory and incidence projective geometry. Proce. ADG 2016, 62\u201377 (2016)","journal-title":"Proce. ADG"},{"key":"9551_CR14","unstructured":"Braun, G., Boutry, P., Narboux, J.: From Hilbert to Tarski. In: Narboux, J., Schreck, P., Streinu, I. (eds.) Proceedings of the Eleventh International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2016, pp. 78\u201396. Strasbourg, France (2016)"},{"key":"9551_CR15","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 (ADG 2012)","author":"G Braun","year":"2012","unstructured":"Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry (ADG 2012). Lecture Notes in Computer Science, vol. 7993, pp. 89\u2013109. Springer, Edinburgh (2012)"},{"issue":"2","key":"9551_CR16","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/s10817-016-9374-4","volume":"58","author":"G Braun","year":"2017","unstructured":"Braun, G., Narboux, J.: A synthetic proof of Pappus\u2019 theorem in Tarski\u2019s geometry. J. Autom. Reason. 58(2), 23 (2017)","journal-title":"J. Autom. Reason."},{"key":"9551_CR17","doi-asserted-by":"crossref","unstructured":"Brun, C., Dufourd, J.-F., Magaud, N.: Formal proof in Coq and derivation of a program in C++ to compute convex hulls. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry (ADG 2012), volume 7993 of Lecture Notes in Computer Science, pp. 71\u201388. Springer Verlag, Berlin (2012)","DOI":"10.1007\/978-3-642-40672-0_6"},{"issue":"1","key":"9551_CR18","doi-asserted-by":"publisher","first-page":"21","DOI":"10.2478\/forma-2018-0003","volume":"26","author":"R Coghetto","year":"2018","unstructured":"Coghetto, R.: Klein-Beltrami model. Part I. Formaliz. Math. 26(1), 21\u201332 (2018)","journal-title":"Formaliz. Math."},{"issue":"1","key":"9551_CR19","doi-asserted-by":"publisher","first-page":"33","DOI":"10.2478\/forma-2018-0004","volume":"26","author":"R Coghetto","year":"2018","unstructured":"Coghetto, R.: Klein-Beltrami model. Part II. Formaliz. Math. 26(1), 33\u201348 (2018)","journal-title":"Formaliz. Math."},{"key":"9551_CR20","volume-title":"Projective Geometry","author":"HSM Coxeter","year":"2003","unstructured":"Coxeter, H.S.M.: Projective Geometry. Springer, Berlin (2003)"},{"issue":"6","key":"9551_CR21","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/s00407-015-0173-9","volume":"70","author":"V De Risi","year":"2016","unstructured":"De Risi, V.: The development of Euclidean axiomatics. Arch. Hist. Exact Sci. 70(6), 591\u2013676 (2016)","journal-title":"Arch. Hist. Exact Sci."},{"issue":"1","key":"9551_CR22","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1016\/j.tcs.2004.05.003","volume":"323","author":"C Dehlinger","year":"2004","unstructured":"Dehlinger, C., Dufourd, J.-F.: Formalizing generalized maps in Coq. Theor. Comput. Sci. 323(1), 351\u2013397 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"9551_CR23","doi-asserted-by":"crossref","unstructured":"Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert\u2019s elementary geometry. In: Automated Deduction in Geometry (ADG 2000), volume 2061 of Lecture Notes in Computer Science, pp. 306\u2013324 (2001)","DOI":"10.1007\/3-540-45410-1_17"},{"key":"9551_CR24","doi-asserted-by":"crossref","unstructured":"Dufourd, J.-F.: A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler\u2019s formula. In: Proceedings of the 2007 ACM Symposium on Applied Computing, SAC \u201907, pp. 757\u2013761. ACM, New York, NY, USA (2007)","DOI":"10.1145\/1244002.1244171"},{"key":"9551_CR25","doi-asserted-by":"crossref","unstructured":"Dufourd, J.-F., Bertot, Y.: Formal study of plane Delaunay triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving\u20192010 (In Federative Logic Conference: FLoC\u20192010), number 6172 in Lecture Notes in Computer Science, pp. 211\u2013226. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_16"},{"key":"9551_CR26","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-45410-1_15","volume-title":"Automated Deduction in Geometry (ADG 2000)","author":"J Fleuriot","year":"2001","unstructured":"Fleuriot, J.: Nonstandard geometric proofs. In: Richter-Gebert, J., Wang, D. (eds.) Automated Deduction in Geometry (ADG 2000), pp. 246\u2013267. Springer, Berlin Heidelberg (2001)"},{"issue":"3","key":"9551_CR27","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1093\/jigpal\/9.3.447","volume":"9","author":"J Fleuriot","year":"2001","unstructured":"Fleuriot, J.: Theorem proving in infinitesimal geometry. Log. J. IGPL 9(3), 447\u2013474 (2001)","journal-title":"Log. J. IGPL"},{"key":"9551_CR28","doi-asserted-by":"crossref","unstructured":"Fleuriot, J.: Exploring the foundations of discrete analytical geometry in Isabelle\/HOL. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry (ADG 2010), volume 6877 of Lecture Notes in Computer Science, pp. 34\u201350. Springer (2010)","DOI":"10.1007\/978-3-642-25070-5_2"},{"issue":"4","key":"9551_CR29","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1090\/S0002-9904-1961-10606-X","volume":"67","author":"H Freudenthal","year":"1961","unstructured":"Freudenthal, H., et al.: K. Borsuk and Wanda Szmielew, foundations of geometry, Euclidean and Bolyai-Lobachevskian geometry, projective geometry. Bull. Am. Math. Soc. 67(4), 342\u2013344 (1961)","journal-title":"Bull. Am. Math. Soc."},{"key":"9551_CR30","unstructured":"Gauss, C.F.: Disquisitiones generales circa superficies curvas. [Mathematical tracts. Typis Dieterichianis (1828)"},{"key":"9551_CR31","unstructured":"Gries, C., Narboux, J., Boutry, P.: Axiomes de continuit\u00e9 en g\u00e9om\u00e9trie neutre : une \u00e9tude m\u00e9canis\u00e9e en Coq. In: Magaud, N., Dargaye, Z. (eds.) Journ\u00e9es Francophones des Langages Applicatifs 2019, Acte des Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2019). Les Rousses, France (2019)"},{"key":"9551_CR32","unstructured":"Gupta, H.N.: Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California, Berkley (1965)"},{"key":"9551_CR33","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-03359-9_3","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Without loss of generality. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, pp. 43\u201359. Springer, Berlin Heidelberg (2009)"},{"key":"9551_CR34","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs, pp. 131\u2013146. Springer, Cham (2013)"},{"key":"9551_CR35","unstructured":"Kahn, G.: Constructive geometry according to Jan von Plato (1995)"},{"key":"9551_CR36","doi-asserted-by":"crossref","unstructured":"Lobatschewsky, N.: Geometrische Untersuchungen zur Theorie der Parallellinien, pp. 159\u2013223. Springer, Vienna (1985)","DOI":"10.1007\/978-3-7091-9511-6_4"},{"key":"9551_CR37","unstructured":"Lorenz, J.F.: Grundriss der Reinen und Angewandten Mathematik. Fleckeisen, Wolfenbuttel(1791)"},{"issue":"3\u20134","key":"9551_CR38","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s10472-014-9434-6","volume":"74","author":"N Magaud","year":"2015","unstructured":"Magaud, N., Chollet, A., Fuchs, L.: Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective. Ann. Math. Artif. Intell. 74(3\u20134), 309\u2013332 (2015)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"8","key":"9551_CR39","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1016\/j.comgeo.2010.06.004","volume":"45","author":"N Magaud","year":"2012","unstructured":"Magaud, N., Narboux, J., Schreck, P.: A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom. 45(8), 406\u2013424 (2012)","journal-title":"Comput. Geom."},{"key":"9551_CR40","unstructured":"Makarios, T.J.M.: A mechanical verification of the independence of Tarski\u2019s Euclidean axiom. Master\u2019s thesis, Victoria University of Wellington (2012)"},{"issue":"3\u20134","key":"9551_CR41","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s10472-014-9436-4","volume":"74","author":"F Mari\u0107","year":"2015","unstructured":"Mari\u0107, F., Simi\u0107, D.: Formalizing complex plane geometry. Ann. Math. Artif. Intell. 74(3\u20134), 271\u2013308 (2015)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9551_CR42","unstructured":"Mari\u0107, F., Simi\u0107, D.: Complex geometry. Archive of Formal Proofs (2019). http:\/\/isa-afp.org\/entries\/Complex_Geometry.html, Formal proof development"},{"volume-title":"Alfred Tarski: Early Work in Poland-Geometry and Teaching","year":"2014","key":"9551_CR43","unstructured":"McFarland, A., McFarland, J., Smith, J. (eds.): Alfred Tarski: Early Work in Poland-Geometry and Teaching. Springer, New York (2014)"},{"key":"9551_CR44","doi-asserted-by":"crossref","unstructured":"Meikle, L., Fleuriot, J.: Formalizing Hilbert\u2019s Grundlagen in Isabelle\/Isar. In: Theorem Proving in Higher Order Logics, pp. 319\u2013334 (2003)","DOI":"10.1007\/10930755_21"},{"key":"9551_CR45","doi-asserted-by":"crossref","unstructured":"Meikle, L., Fleuriot, J.: Mechanical theorem proving in computational geometry. In: Hong, H., Wang, D. (eds.) Automated Deduction in Geometry (ADG 2004), pp. 1\u201318. Springer, Berlin Heidelberg (2006)","DOI":"10.1007\/11615798_1"},{"key":"9551_CR46","doi-asserted-by":"crossref","unstructured":"Narboux, J.: Mechanical theorem proving in Tarski\u2019s geometry. In: Eugenio, F., Roanes, L. (eds) Automated Deduction in Geometry (ADG 2006), volume 4869 of Lecture Notes in Computer Science, pp. 139\u2013156. Springer, Pontevedra, Spain (2007)","DOI":"10.1007\/978-3-540-77356-6_9"},{"key":"9551_CR47","unstructured":"Narboux, J., Jani\u010di\u0107, P., Fleuriot, J.: Computer-assisted theorem proving in synthetic geometry. In: Sitharam, M., St. John, A., Sidman, J. (eds.) Handbook of Geometric Constraint Systems Principles, chapter\u00a02, pp. 25\u201373. Chapman and Hall\/CRC (2018)"},{"key":"9551_CR48","volume-title":"Visual Complex Analysis","author":"T Needham","year":"1998","unstructured":"Needham, T.: Visual Complex Analysis. Oxford University Press, Oxford (1998)"},{"key":"9551_CR49","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Programming and Proving in Isabelle\/HOL (2013)","DOI":"10.1007\/978-3-319-10542-0_6"},{"key":"9551_CR50","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Berlin (2002)"},{"key":"9551_CR51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-65611-8","volume-title":"Vorlesung \u00fcber Neuere Geometrie","author":"M Pasch","year":"1976","unstructured":"Pasch, M.: Vorlesung \u00fcber Neuere Geometrie. Springer, Berlin (1976)"},{"issue":"3","key":"9551_CR52","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"LC Paulson","year":"1986","unstructured":"Paulson, L.C.: Natural deduction as higher-order resolution. J Log Program 3(3), 237\u2013258 (1986)","journal-title":"J Log Program"},{"issue":"3","key":"9551_CR53","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"LC Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. J Autom Reason 5(3), 363\u2013397 (1989)","journal-title":"J Autom Reason"},{"key":"9551_CR54","doi-asserted-by":"crossref","unstructured":"Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R., Jackson, P. (eds.) Theorem Proving in Higher Order Logics, pp. 346\u2013361. Springer, Berlin Heidelberg (2001)","DOI":"10.1007\/3-540-44755-5_24"},{"key":"9551_CR55","doi-asserted-by":"crossref","unstructured":"Puitg, F., Dufourd, J.-F.: Formal specification and theorem proving breakthroughs in geometric modeling. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics, pp. 401\u2013422. Springer, Berlin Heidelberg (1998)","DOI":"10.1007\/BFb0055149"},{"key":"9551_CR56","unstructured":"Richter, W.: Formalizing Rigorous Hilbert axiomatic geometry proofs in the proof assistant Hol light. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.363.2373&rep=rep1&type=pdf"},{"issue":"2","key":"9551_CR57","doi-asserted-by":"publisher","first-page":"167","DOI":"10.2478\/forma-2014-0017","volume":"22","author":"W Richter","year":"2014","unstructured":"Richter, W., Grabowski, A., Alama, J.: Tarski geometry axioms. Formaliz. Math. 22(2), 167\u2013176 (2014)","journal-title":"Formaliz. Math."},{"key":"9551_CR58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-24861-4","volume-title":"\u00dcber die Hypothesen, welche der Geometrie zu Grunde liegen","author":"B Riemann","year":"1921","unstructured":"Riemann, B., Weyl, Hermann: \u00dcber die Hypothesen, welche der Geometrie zu Grunde liegen. Springer, Berlin (1921)"},{"key":"9551_CR59","unstructured":"Saccheri, G.G.: Euclides ab omni naevo vindicatus. Mediolani: Ex typographia Pauli Antonio Montani (1733)"},{"key":"9551_CR60","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69418-9","volume-title":"Metamathematische Methoden in der Geometrie","author":"W Schwabh\u00e4user","year":"1983","unstructured":"Schwabh\u00e4user, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983)"},{"key":"9551_CR61","volume-title":"Geometry of Complex Numbers: Circle Geometry, Moebius Transformation, Non-euclidean Geometry","author":"H Schwerdtfeger","year":"1979","unstructured":"Schwerdtfeger, H.: Geometry of Complex Numbers: Circle Geometry, Moebius Transformation, Non-euclidean Geometry. North Chelmsford, North Chelmsford (1979)"},{"key":"9551_CR62","unstructured":"Scott, P.: Mechanising Hilbert\u2019s foundations of geometry in Isabelle. Master\u2019s thesis, University of Edinburgh (2008)"},{"key":"9551_CR63","doi-asserted-by":"crossref","unstructured":"Scott, P., Fleuriot, J.: An investigation of Hilbert\u2019s implicit reasoning through proof discovery in idle-time. In: Proceedings of the Seventh International Workshop on Automated Deduction in Geometry, pp. 182\u2013200 (2010)","DOI":"10.1007\/978-3-642-25070-5_11"},{"key":"9551_CR64","unstructured":"Simi\u0107, D., Mari\u0107, F., Boutry, P.: Poincar\u00e9 disc model. Archive of Formal Proofs, (2019). http:\/\/isa-afp.org\/entries\/Poincare_Disc.html, Formal proof development"},{"key":"9551_CR65","doi-asserted-by":"crossref","unstructured":"Stojanovi\u0107\u00a0\u0110ur\u0111evi\u0107, S., Narboux, J., Jani\u010di\u0107, P.: Automated generation of machine verifiable and readable proofs: a case study of Tarski\u2019s geometry. Ann. Math. Artific. Intell. pp. 249\u2013269 (2015)","DOI":"10.1007\/s10472-014-9443-5"},{"issue":"2","key":"9551_CR66","doi-asserted-by":"publisher","first-page":"175","DOI":"10.2307\/421089","volume":"5","author":"A Tarski","year":"1999","unstructured":"Tarski, A., Givant, S.: Tarski\u2019s system of geometry. Bull. Symbol. Log. 5(2), 175\u2013214 (1999)","journal-title":"Bull. Symbol. Log."},{"issue":"2","key":"9551_CR67","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0168-0072(95)00005-2","volume":"76","author":"J von Plato","year":"1995","unstructured":"von Plato, J.: The axioms of constructive geometry. Ann. Pure Appl. Log. 76(2), 169\u2013200 (1995)","journal-title":"Ann. Pure Appl. Log."},{"key":"9551_CR68","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09551-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09551-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09551-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,29]],"date-time":"2021-04-29T23:31:29Z","timestamp":1619739089000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09551-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,30]]},"references-count":68,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["9551"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09551-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,4,30]]},"assertion":[{"value":"6 June 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 April 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}