{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:03:03Z","timestamp":1777424583100,"version":"3.51.4"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2015,1,7]],"date-time":"2015-01-07T00:00:00Z","timestamp":1420588800000},"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-9443-5","type":"journal-article","created":{"date-parts":[[2015,1,6]],"date-time":"2015-01-06T15:45:10Z","timestamp":1420559110000},"page":"249-269","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Automated generation of machine verifiable and readable proofs: A case study of Tarski\u2019s geometry"],"prefix":"10.1007","volume":"74","author":[{"given":"Sana Stojanovi\u0107","family":"\u00d0ur\u0111evi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Narboux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Predrag","family":"Jani\u010di\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,1,7]]},"reference":[{"issue":"4","key":"9443_CR1","doi-asserted-by":"crossref","first-page":"700","DOI":"10.1017\/S1755020309990098","volume":"2","author":"J Avigad","year":"2009","unstructured":"Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid\u2019s elements. Rev. Symb. Log. 2(4), 700\u2013768 (2009)","journal-title":"Rev. Symb. Log."},{"key":"9443_CR2","doi-asserted-by":"crossref","unstructured":"Beeson, M.: Proof and computation in geometry. In: Automated Deduction in Geometry \u2013 ADG 2012, volume 7993 of Lecture Notes in Computer Science, pp. 1\u201330. Springer (2013)","DOI":"10.1007\/978-3-642-40672-0_1"},{"key":"9443_CR3","doi-asserted-by":"crossref","unstructured":"Beeson, M., Wos, L.: OTTER Proofs in Tarskian geometry. In: Automated Reasoning - 7th International Joint Conference, IJCAR 2014, volume 8562 of Lecture Notes in Computer Science, pp. 495\u2013510. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_38"},{"key":"9443_CR4","doi-asserted-by":"crossref","unstructured":"Blanchette, J. C. : Redirecting proofs by Contradiction. In: Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013, volume 14 of EPiC Series, pp. 11\u201326. EasyChair (2013)","DOI":"10.29007\/wm8b"},{"key":"9443_CR5","doi-asserted-by":"crossref","unstructured":"Bezem, M., Coquand, T.: Automating coherent logic. In: 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning \u2014 LPAR 2005, volume 3835 of Lecture Notes in Computer Science. Springer-Verlag (2005)","DOI":"10.1007\/11591191_18"},{"key":"9443_CR6","doi-asserted-by":"crossref","unstructured":"Bezem, M, Hendriks, D. : On the mechanization of the proof of Hessenberg\u2019s theorem in coherent logic. J. Autom. Reason. 40(1) (2008)","DOI":"10.1007\/s10817-007-9086-x"},{"issue":"1","key":"9443_CR7","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51 (1), 109\u2013128 (2013)","journal-title":"J. Autom. Reason."},{"key":"9443_CR8","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Frontiers of Combining Systems, 8th International Symposium, Proceedings, volume 6989 of Lecture Notes in Computer Science, pp. 12\u201327. Springer (2011)","DOI":"10.1007\/978-3-642-24364-6_2"},{"key":"9443_CR9","unstructured":"Boutry, P., Narboux, J., Schreck, P., Braun, G.: A short note about case distinctions in Tarski\u2019s geometry. 10th International Workshop on Automated Deduction in Geometry (ADG 2014), pp. 51-66. TR 2014\/01, University of Coimbra (2014)"},{"key":"9443_CR10","unstructured":"Boutry, P., Narboux, J., Schreck, P., Braun, G.: Using small scale automation to improve both accessibility and readability of formal proofs in geometry. 10th International Workshop on Automated Deduction in Geometry (ADG 2014), pp. 31-50. TR 2014\/01, University of Coimbra (2014)"},{"key":"9443_CR11","doi-asserted-by":"crossref","unstructured":"Braun, G., Narboux, J.: From Tarski to Hilbert. In: Automated Deduction in Geometry \u2013 ADG 2012 volume 7993 of Lecture Notes in Computer Science, pp. 89\u2013109. Springer (2013)","DOI":"10.1007\/978-3-642-40672-0_7"},{"key":"9443_CR12","doi-asserted-by":"crossref","unstructured":"Fisher, J., Bezem, M.: Skolem machines and geometric logic. In: 4th International Colloquium on Theoretical Aspects of Computing \u2014 ICTAC 2007, volume 4711 of Lecture Notes in Computer Science. Springer-Verlag (2007)","DOI":"10.1007\/978-3-540-75292-9_14"},{"key":"9443_CR13","unstructured":"Ganesalingam, M., Gowers, W.T.: A fully automatic problem solver with human-style output. CoRR, abs\/1309.4501 (2013)"},{"key":"9443_CR14","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O\u2019Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the Odd Order theorem. In: 4th Conference on Interactive Theorem Proving \u2013 ITP 2013 volume 7998 of Lecture Notes in Computer Science, pp. 163\u2013179. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"9443_CR15","volume-title":"Contributions to the axiomatic foundations of geometry. PhD thesis","author":"NG Haragauri","year":"1965","unstructured":"Haragauri N.G.: Contributions to the axiomatic foundations of geometry. PhD thesis. University of California, Berkley (1965)"},{"key":"9443_CR16","unstructured":"Hales T.C.: Introduction to the Flyspeck project. In: Mathematics, Algorithms, Proofs, volume 05021 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany, p 2006"},{"key":"9443_CR17","volume-title":"Grundlagen der Geometrie","author":"D Hilbert","year":"1899","unstructured":"Hilbert, D.: Grundlagen der Geometrie. Baedeker, Leipzig (1899)"},{"key":"9443_CR18","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. CoRR, abs\/1211.7012 (2012)"},{"key":"9443_CR19","unstructured":"Makarios, T.: A further simplification of Tarski\u2019s axioms of geometry. CoRR, abs\/1306.0066 (2013)"},{"key":"9443_CR20","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":"9443_CR21","doi-asserted-by":"crossref","unstructured":"Meikle, L., Fleuriot, J.: Mechanical theorem proving in computation geometry. In: Automated Deduction in Geometry \u2013 ADG 04, volume 3763 of Lecture Notes in Computer Science, pp. 1\u201318. Springer-Verlag, November (2005)","DOI":"10.1007\/11615798_1"},{"key":"9443_CR22","doi-asserted-by":"crossref","unstructured":"Narboux, J.: Mechanical theorem proving in Tarski\u2019s geometry. In: Proceedings of Automatic Deduction in Geometry 06, volume 4869 of Lecture Notes in Artificial Intelligence, pp. 139\u2013156. Springer-Verlag (2007)","DOI":"10.1007\/978-3-540-77356-6_9"},{"key":"9443_CR23","unstructured":"Polonsky, A.: Proofs, Types and Lambda Calculus. PhD thesis, University of Bergen (2011)"},{"issue":"1","key":"9443_CR24","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF00245024","volume":"5","author":"A Quaife","year":"1989","unstructured":"Quaife, A.: Automated development of Tarski\u2019s geometry. J. Autom. Reason. 5(1), 97\u2013118 (1989)","journal-title":"J. Autom. Reason."},{"issue":"2-3","key":"9443_CR25","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun. 15(2-3), 91\u2013110 (2002)","journal-title":"AI Commun."},{"key":"9443_CR26","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine oriented logic based on the resolution principle. J. ACM 12, 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"2-3","key":"9443_CR27","first-page":"111","volume":"15","author":"Stephan Schulz","year":"2002","unstructured":"Stephan Schulz: E - a brainiac theorem prover. AI Commun 15(2-3), 111\u2013126 (2002)","journal-title":"AI Commun"},{"key":"9443_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69418-9","volume-title":"Metamathematische Methoden in der Geometrie","author":"W Schwabhuser","year":"1983","unstructured":"Schwabhuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin (1983)"},{"key":"9443_CR29","doi-asserted-by":"crossref","unstructured":"Stojanovi\u0107, S., Narboux, J., Bezem, M., Jani\u010di\u0107, P.: A vernacular for coherent logic. In: Conferences on Intelligent Computer Mathematics, volume 8543 of Lecture Notes in Computer Science, pp. 388\u2013403. Springer (2014)","DOI":"10.1007\/978-3-319-08434-3_28"},{"key":"9443_CR30","doi-asserted-by":"crossref","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: Automated Deduction in Geometry - ADG 2010, volume 6877 of Lecture Notes in Computer Science. Springer (2011)","DOI":"10.1007\/978-3-642-25070-5_12"},{"issue":"4","key":"9443_CR31","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"key":"9443_CR32","doi-asserted-by":"crossref","unstructured":"Tankink, C., Kaliszyk, C., Urban, J., Geuvers, H.: Communicating formal proofs: The case of Flyspeck. In: Interactive Theorem Proving - 4th International Conference, Proceedings, volume 7998 of Lecture Notes in Computer Science, pp. 451\u2013456. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_32"},{"key":"9443_CR33","doi-asserted-by":"crossref","unstructured":"Tarski, A. : What is elementary geometry? . In: P. Suppes , L. Henkin, A. Tarski (eds.) The axiomatic Method, with special reference to Geometry and Physics, pp 16\u201329. Amsterdam , North-Holland (1959)","DOI":"10.1016\/S0049-237X(09)70017-5"},{"key":"9443_CR34","doi-asserted-by":"crossref","unstructured":"Tarski, A., Givant, S.: Tarski\u2019s system of geometry. Bull. Symb. Log. 5(2) (1999)","DOI":"10.2307\/421089"},{"key":"9443_CR35","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: Spass version 3.5. In: Automated Deduction - CADE-22 Proceedings, volume 5663 of Lecture Notes in Computer Science, pp. 140\u2013145. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"9443_CR36","doi-asserted-by":"crossref","unstructured":"Markus, W.: Isar - a generic interpretative approach to readable formal proof documents. In: Theorem Proving in Higher Order Logics (TPHOLs\u201999), volume 1690 of Lecture Notes in Computer Science, pp. 167\u2013184. Springer (1999)","DOI":"10.1007\/3-540-48256-3_12"},{"key":"9443_CR37","doi-asserted-by":"crossref","unstructured":"Wiedijk, F. (ed.): The seventeen provers of the World, volume 3600 of Lecture Notes in Computer Science Springer (2006)","DOI":"10.1007\/11542384"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9443-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-014-9443-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9443-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,16]],"date-time":"2025-05-16T02:06:50Z","timestamp":1747361210000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-014-9443-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,7]]},"references-count":37,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["9443"],"URL":"https:\/\/doi.org\/10.1007\/s10472-014-9443-5","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,7]]}}}