{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,8]],"date-time":"2024-08-08T12:40:12Z","timestamp":1723120812242},"reference-count":81,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2020,6,25]],"date-time":"2020-06-25T00:00:00Z","timestamp":1593043200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,25]],"date-time":"2020-06-25T00:00:00Z","timestamp":1593043200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s11786-020-00489-7","type":"journal-article","created":{"date-parts":[[2020,6,25]],"date-time":"2020-06-25T11:03:03Z","timestamp":1593082983000},"page":"673-692","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Automated Deduction and Knowledge Management in Geometry"],"prefix":"10.1007","volume":"14","author":[{"given":"Pedro","family":"Quaresma","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,6,25]]},"reference":[{"key":"489_CR1","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development (Coq\u2019Art: The Calculus of Inductive Constructions). Springer, EATCS (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"489_CR2","doi-asserted-by":"crossref","unstructured":"Botana, F., Hohenwarter, M., Jani\u010di\u0107, P., Kov\u00e1cs, Z., Petrovi\u0107, Ivan, R., Tom\u00e1s, W.S.: Automated theorem proving in GeoGebra: current achievements. J. Autom. Reason. 55(1), 39\u201359 (2015)","DOI":"10.1007\/s10817-015-9326-4"},{"key":"489_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Volume 11429 of LNCS. Springer, 2019. Held as Part of ETAPS 2019, Prague, Czech Republic, April 6\u201311 (2019)","DOI":"10.1007\/978-3-030-17502-3"},{"key":"489_CR4","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-319-99957-9_15","volume-title":"Artificial Intelligence and Symbolic Computation","author":"F Botana","year":"2018","unstructured":"Botana, F., Kov\u00e1cs, Z., Recio, T.: Towards an automated geometer. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) Artificial Intelligence and Symbolic Computation, pp. 215\u2013220. Springer, Cham (2018)"},{"key":"489_CR5","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0360-1315(01)00089-6","volume":"38","author":"F Botana","year":"2002","unstructured":"Botana, F., Valcarce, J.L.: A dynamic-symbolic interface for geometric theorem discovery. Comput. Educ. 38, 21\u201335 (2002)","journal-title":"Comput. Educ."},{"key":"489_CR6","unstructured":"Baeta, N., Quaresma, P.: The full angle method on the OpenGeoProver. In: Lange, C., Aspinall, D., Carette, J., Davenport, J., Kohlhase, A., Kohlhase, M., Libbrecht, P., Quaresma, P., Rabe, F., Sojka, P., Whiteside, I., Windsteiger, W. (eds.) MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, number 1010 in CEUR Workshop Proceedings, Aachen (2013)"},{"key":"489_CR7","doi-asserted-by":"crossref","unstructured":"Baeta, N., Quaresma, P.: Towards ranking geometric automated theorem provers. In: Quaresma, P., Neuper, W. (eds.) Proceedings 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018, volume 290 of Electronic Proceedings in Theoretical Computer Science, pp. 30\u201337. Open Publishing Association (2019)","DOI":"10.4204\/EPTCS.290.3"},{"key":"489_CR8","doi-asserted-by":"crossref","unstructured":"Baeta, N., Quaresma, P., Kov\u00e1cs, Z.: Towards a geometry automated provers competition. In: Proceedings 8th International Workshop on Theorem proving Components for Educational Software, Volume 313 of Electronic Proceedings in Theoretical Computer Science, pp. 93\u2013100, February 2020. (ThEdu\u201919), Natal, Brazil, 25th August (2019)","DOI":"10.4204\/EPTCS.313.6"},{"key":"489_CR9","unstructured":"Budd Rowe, M.: Wait-time and rewards as instructional variables: Their influence on language, logic, and fate control. Technical report, National Association for Research in Science Teaching (1972)"},{"issue":"1","key":"489_CR10","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1177\/002248718603700110","volume":"37","author":"M Budd Rowe","year":"1986","unstructured":"Budd Rowe, M.: Wait time: slowing down may be a way of speeding up!. J. Teach. Educ. 37(1), 43\u201350 (1986)","journal-title":"J. Teach. Educ."},{"key":"489_CR11","volume-title":"All About Maude\u2014A High-Performance Logical Framework (Pb). Lecture Notes in Computer Science","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude\u2014A High-Performance Logical Framework (Pb). Lecture Notes in Computer Science, vol. 4350. Springer, New York (2007)"},{"key":"489_CR12","doi-asserted-by":"crossref","first-page":"707","DOI":"10.1016\/B978-044450813-3\/50013-8","volume-title":"Handbook of Automated Reasoning","author":"S-C Chou","year":"2001","unstructured":"Chou, S.-C., Gao, X.-S.: Automated reasoning in geometry. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 707\u2013749. Elsevier, Amsterdam (2001)"},{"key":"489_CR13","doi-asserted-by":"crossref","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry","author":"S-C Chou","year":"1994","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)"},{"issue":"13","key":"489_CR14","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00283133","volume":"17","author":"S-C Chou","year":"1996","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated generation of readable proofs with geometric invariants, I. Multiple and shortest proof generation. J. Autom. Reason. 17(13), 325\u2013347 (1996)","journal-title":"J. Autom. Reason."},{"issue":"13","key":"489_CR15","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF00283134","volume":"17","author":"S-C Chou","year":"1996","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated generation of readable proofs with geometric invariants, II. Theorem proving with full-angles. J. Autom. Reason. 17(13), 349\u2013370 (1996)","journal-title":"J. Autom. Reason."},{"key":"489_CR16","first-page":"278","volume-title":"Intelligent Computer Mathematics. Number 6167 in LNCS","author":"X Chen","year":"2010","unstructured":"Chen, X.: Electronic geometry textbook: a geometric textbook knowledge management system. Intelligent Computer Mathematics. Number 6167 in LNCS, pp. 278\u2013292. Springer, Berlin (2010)"},{"issue":"2","key":"489_CR17","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1007\/s11424-014-0316-0","volume":"27","author":"X Chen","year":"2014","unstructured":"Chen, X.: Representation and automated transformation of geometric statements. J. Syst. Sci. Complex. 27(2), 382\u2013412 (2014)","journal-title":"J. Syst. Sci. Complex."},{"key":"489_CR18","unstructured":"Chou, S.C.: Proving and discovering geometry theorems using Wu\u2019s method. Ph.D. thesis, The University of Texas, Austin (1985)"},{"key":"489_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-009-4037-6","volume-title":"Mechanical Geometry Theorem Proving","author":"S-C Chou","year":"1987","unstructured":"Chou, S.-C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company, Dordrecht (1987)"},{"key":"489_CR20","doi-asserted-by":"crossref","first-page":"432","DOI":"10.1007\/978-3-642-31374-5_31","volume-title":"Intelligent Computer Mathematics","author":"X Chen","year":"2012","unstructured":"Chen, X., Li, W., Luo, J., Wang, D.: Open geometry textbook: a case study of knowledge acquisition via collective intelligence. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) Intelligent Computer Mathematics, pp. 432\u2013437. Springer, Berlin (2012)"},{"key":"489_CR21","volume-title":"Graph-Based Knowledge Representation: Computational Foundations of Conceptual Graphs. Advanced Information and Knowledge Processing Series","author":"M Chein","year":"2009","unstructured":"Chein, M., Mugnier, M.-L.: Graph-Based Knowledge Representation: Computational Foundations of Conceptual Graphs. Advanced Information and Knowledge Processing Series. Springer, New York (2009)"},{"key":"489_CR22","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, May 20\u201323, 1975. Lecture Notes in Computer Science, vol. 33. Springer, Berlin (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"issue":"4","key":"489_CR23","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/BF00248249","volume":"2","author":"H Coelho","year":"1986","unstructured":"Coelho, H., Pereira, L.M.: Automated reasoning in geometry theorem proving with Prolog. J. Autom. Reason. 2(4), 329\u2013390 (1986)","journal-title":"J. Autom. Reason."},{"key":"489_CR24","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.datak.2011.10.004","volume":"73","author":"X Chen","year":"2012","unstructured":"Chen, X., Wang, D.: Management of geometric knowledge in textbooks. Data Knowl. Eng. 73, 43\u201357 (2012)","journal-title":"Data Knowl. Eng."},{"key":"489_CR25","first-page":"41","volume-title":"Selected Papers on Automath. Volume 133 of Studies in Logic and the Foundations of Mathematics","author":"NG de Bruijn","year":"1994","unstructured":"de Bruijn, N.G.: A survey of the project Automath. Selected Papers on Automath. Volume 133 of Studies in Logic and the Foundations of Mathematics, pp. 41\u2013161. North-Holland, Amsterdam (1994)"},{"key":"489_CR26","doi-asserted-by":"crossref","unstructured":"Dhar, S., Roy, S., Das, S.: A Critical Survey of Mathematical Search Engines. In: Computational Intelligence, Communications, and Business Analytics, pp. 193\u2013207. Springer, New York (2019)","DOI":"10.1007\/978-981-13-8581-0_16"},{"key":"489_CR27","doi-asserted-by":"crossref","unstructured":"Font, L., Richard, P.R., Gagnon, M.: Improving qed-tutrix by automating the generation of proofs. In: Quaresma, P., Neuper, W. (eds.) Proceedings 6th International Workshop on Theorem Proving Components for Educational Software, Gothenburg, Sweden, 6 Aug 2017, volume 267 of Electronic Proceedings in Theoretical Computer Science, pp. 38\u201358. Open Publishing Association (2018)","DOI":"10.4204\/EPTCS.267.3"},{"key":"489_CR28","unstructured":"Gelernter, H.: Realization of a geometry-theorem proving machine. In: Computers & Thought, 2nd edn., pp. 134\u2013152. MIT Press, Cambridge (1995)"},{"key":"489_CR29","doi-asserted-by":"crossref","unstructured":"Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of the geometry theorem machine. In: Papers Presented at the May 3\u20135, 1960, Western Joint IRE-AIEE-ACM Computer Conference, IRE-AIEE-ACM \u201960 (Western), pp. 143\u2013149. ACM, New York (1960)","DOI":"10.1145\/1460361.1460381"},{"key":"489_CR30","unstructured":"Gagnon, M., Leduc, N., Richard, P.R., Tessier-Baillargeon, M.: Qed-tutrix: creating and expanding a problem database towards personalized problem itineraries for proof learning in geometry. In: Proceedings of the Tenth Congress of the European Society for Research in Mathematics Education (CERME10) (2017)"},{"issue":"1\u20132","key":"489_CR31","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1012737223465","volume":"44","author":"G Hanna","year":"2000","unstructured":"Hanna, G.: Proof, explanation and exploration: an overview. Educ. Stud. Math. 44(1\u20132), 5\u201323 (2000)","journal-title":"Educ. Stud. Math."},{"key":"489_CR32","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139644082","volume-title":"Search User Interfaces","author":"MA Hearst","year":"2009","unstructured":"Hearst, M.A.: Search User Interfaces. Cambridge University Press, Cambridge (2009)"},{"key":"489_CR33","doi-asserted-by":"crossref","unstructured":"Han, T.A., Pereira, L.M., Lenaerts, T.: Modelling and influencing the AI bidding war: a research agenda. In: AAAI\/ACM Conference on AI, Ethics and Society 2019, vol. 1 (2019)","DOI":"10.1145\/3306618.3314265"},{"key":"489_CR34","first-page":"298","volume-title":"CICM 2014, Volume 8543 of LNAI","author":"Y Haralambous","year":"2014","unstructured":"Haralambous, Y., Quaresma, P.: Querying geometric figures using a controlled language, ontological graphs and dependency lattices. In: Watt, S., et al. (eds.) CICM 2014, Volume 8543 of LNAI, pp. 298\u2013311. Springer, New York (2014)"},{"key":"489_CR35","unstructured":"Haralambous, Y., Quaresma, P.: Geometric search in TGTP. In: Li, H. (ed.) Proceedings of the 12th International Conference on Automated Deduction in Geometry. SMS International (2018)"},{"volume-title":"Proof Technology in Mathematics Research and Teaching","year":"2019","key":"489_CR36","unstructured":"Hanna, G., Reid, D., de Villiers, M. (eds.): Proof Technology in Mathematics Research and Teaching. Springer, New York (2019)"},{"key":"489_CR37","first-page":"58","volume-title":"Mathematical Software\u2014ICMS 2006, Volume 4151 of Lecture Notes in Computer Science","author":"P Jani\u010di\u0107","year":"2006","unstructured":"Jani\u010di\u0107, P.: GCLC\u2014a tool for constructive euclidean geometry and more than that. In: Iglesias, A., Takayama, N. (eds.) Mathematical Software\u2014ICMS 2006, Volume 4151 of Lecture Notes in Computer Science, pp. 58\u201373. Springer, New York (2006)"},{"issue":"4","key":"489_CR38","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/s10817-010-9209-7","volume":"48","author":"P Jani\u010di\u0107","year":"2012","unstructured":"Jani\u010di\u0107, P., Narboux, J., Quaresma, P.: The Area method: a recapitulation. J. Autom. Reason. 48(4), 489\u2013532 (2012)","journal-title":"J. Autom. Reason."},{"key":"489_CR39","first-page":"145","volume-title":"Automated Reasoning, Volume 4130 of Lecture Notes in Computer Science","author":"P Jani\u010di\u0107","year":"2006","unstructured":"Jani\u010di\u0107, P., Quaresma, P.: System description: GCLCprover + GeoThms. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning, Volume 4130 of Lecture Notes in Computer Science, pp. 145\u2013150. Springer, New York (2006)"},{"key":"489_CR40","first-page":"39","volume-title":"Automated Deduction in Geometry, Volume 4869 of Lecture Notes in Computer Science","author":"P Jani\u010di\u0107","year":"2007","unstructured":"Jani\u010di\u0107, P., Quaresma, P.: Automatic verification of regular constructions in dynamic geometry systems. In: Botana, F., Recio, T. (eds.) Automated Deduction in Geometry, Volume 4869 of Lecture Notes in Computer Science, pp. 39\u201351. Springer, New York (2007)"},{"key":"489_CR41","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry theorem proving using Hilbert\u2019s nullstellensatz. In: SYMSAC \u201986: Proceedings of the fifth ACM symposium on Symbolic and algebraic computation, pp. 202\u2013208. ACM Press, New York (1986)","DOI":"10.1145\/32439.32479"},{"issue":"4","key":"489_CR42","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1016\/S0747-7171(86)80007-4","volume":"2","author":"D Kapur","year":"1986","unstructured":"Kapur, D.: Using Gr\u00f6bner bases to reason about geometry problems. J. Symb. Comput. 2(4), 399\u2013408 (1986)","journal-title":"J. Symb. Comput."},{"key":"489_CR43","unstructured":"Kortenkamp, U., Dohrmann, C., Kreis, Y., Dording, C., Libbrecht, P., Mercat, C.: Using the Intergeo platform for teaching and research. In: Proceedings of the 9th International Conference on Technology in Mathematics Teaching (ICTMT-9) (2009)"},{"key":"489_CR44","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-319-21362-0_4","volume-title":"Automated Deduction in Geometry","author":"Z Kov\u00e1cs","year":"2015","unstructured":"Kov\u00e1cs, Z.: The relation tool in geogebra 5. In: Botana, F., Quaresma, P. (eds.) Automated Deduction in Geometry, pp. 53\u201371. Springer, New York (2015)"},{"key":"489_CR45","unstructured":"Leduc, N.: QED-Tutrix : syst\u00e8me tutoriel intelligent pour l\u2019accompagnement d\u2019\u00e9l\u00e8ves en situation de r\u00e9solution de probl\u00e8mes de d\u00e9monstration en g\u00e9om\u00e9trie plane. Ph.D. thesis, \u00c9cole polytechnique de Montr\u00e9al (2016)"},{"key":"489_CR46","unstructured":"Lemoine, \u00c9.: G\u00e9om\u00e9trographie ou Art des constructions g\u00e9om\u00e9triques, volume\u00a018 of Phys-Math\u00e9matique. Scentia, Sydney (1902)"},{"key":"489_CR47","first-page":"205","volume-title":"Mathematics Mechanization and Applications","author":"H Li","year":"2000","unstructured":"Li, H.: Clifford algebra approaches to mechanical geometry theorem proving. In: Gao, X.-S., Wang, D. (eds.) Mathematics Mechanization and Applications, pp. 205\u2013299. Academic Press, San Diego (2000)"},{"key":"489_CR48","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1017\/S0013091500001565","volume":"12","author":"JS Mackay","year":"1893","unstructured":"Mackay, J.S.: The geometrography of euclid\u2019s problems. Proc. Edinb. Math. Soc. 12, 2\u201316 (1893)","journal-title":"Proc. Edinb. Math. Soc."},{"key":"489_CR49","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-642-16310-4_2","volume-title":"Rewriting Logic and Its Applications","author":"J Meseguer","year":"2010","unstructured":"Meseguer, J.: Twenty years of rewriting logic. In: \u00d6lveczky, P.C. (ed.) Rewriting Logic and Its Applications, pp. 15\u201317. Springer, Berlin (2010)"},{"key":"489_CR50","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/s10472-018-9590-1","volume":"85","author":"Z Kov\u00e1cs","year":"2019","unstructured":"Kov\u00e1cs, Z., Nikoli\u0107, P., Mladen, J., Marinkovi\u0107, V.: Portfolio theorem proving and prover runtime prediction for geometry. Ann. Math. Artif. Intell. 85, 119\u2013146 (2019)","journal-title":"Ann. Math. Artif. Intell."},{"key":"489_CR51","doi-asserted-by":"crossref","unstructured":"Moraes, T.G., Santoro, F.M., Borges, M.R.S.: Tabul\u00e6: educational groupware for learning geometry. In: Fifth IEEE International Conference on Advanced Learning Technologies, 2005. ICALT 2005, pp. 750\u2013754 (2005)","DOI":"10.1109\/ICALT.2005.251"},{"key":"489_CR52","unstructured":"Moriy\u00f3n, R., Saiz, F., Mora, M.: GeoThink: An Environment for Guided Collaborative Learning of Geometry, volume\u00a04 of Nuevas Ideas en Inform\u00e1tica Educativa, pp. 200\u20132008. J. S\u00e1nchez (ed.), Santiago de Chile (2008)"},{"issue":"2","key":"489_CR53","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/s00165-009-0117-8","volume":"22","author":"P Mathis","year":"2010","unstructured":"Mathis, P., Thierry, S.E.B.: A formalization of geometric constraint systems and their decomposition. Formal Asp. Comput. 22(2), 129\u2013151 (2010)","journal-title":"Formal Asp. Comput."},{"key":"489_CR54","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10817-007-9071-4","volume":"39","author":"J Narboux","year":"2007","unstructured":"Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reason. 39, 161\u2013180 (2007)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"489_CR55","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1023\/B:STUD.0000039031.11852.66","volume":"77","author":"V Pambuccian","year":"2004","unstructured":"Pambuccian, V.: The simplest axiom system for plane hyperbolic geometry. Stud. Log. 77(3), 385\u2013411 (2004)","journal-title":"Stud. Log."},{"key":"489_CR56","volume-title":"Geometrografia 1","author":"VA Pinheiro","year":"1974","unstructured":"Pinheiro, V.A.: Geometrografia 1. Bahiense, Rio de Janeiro (1974)"},{"key":"489_CR57","unstructured":"Petrovi\u0107, I., Kov\u00e1cs, Z., Weitzhofer, S., Hohenwarter, M., Jani\u010di\u0107, P.: Extending GeoGebra with automated theorem proving by using OpenGeoProver. In: Proceedings CADGME 2012, Novi Sad, Serbia (2012)"},{"key":"489_CR58","unstructured":"Quaresma, P., Baeta, N.: Geometry automated theorem provers systems competition 0.2 report. Techreport\u00a01, CISUC (2019)"},{"key":"489_CR59","unstructured":"Quaresma, P., Nuno, B.: Current status of the I2GATP common format. In: Botana, F., Quaresma, P. (eds.) Proceedings ADG 2014, Volume 2014 of CISUC Technical Report, pp. 67\u201374. CISUC (2014)"},{"key":"489_CR60","volume-title":"Proof Technology in Mathematics Research and Teaching","author":"P Quaresma","year":"2019","unstructured":"Quaresma, P., Santos, V.: Computer-generated geometry proofs in a learning context. In: Hanna, G., Reid, D.A., de Villiers, M. (eds.) Proof Technology in Mathematics Research and Teaching. Springer, New York (2019)"},{"key":"489_CR61","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.jsc.2018.12.004","volume":"97","author":"P Quaresma","year":"2020","unstructured":"Quaresma, P., Santos, V., Graziani, P., Baeta, N.: Taxonomy of geometric problems. J. Symb. Comput. 97, 31\u201355 (2020)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"489_CR62","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/s10639-017-9597-y","volume":"23","author":"P Quaresma","year":"2018","unstructured":"Quaresma, P., Santos, V., Mari\u0107, M.: WGL, a web laboratory for geometry. Educ. Inf. Technol. 23(1), 237\u2013252 (2018)","journal-title":"Educ. Inf. Technol."},{"key":"489_CR63","doi-asserted-by":"publisher","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, 97\u2013118 (1989). https:\/\/doi.org\/10.1007\/BF00245024","journal-title":"J. Autom. Reason."},{"key":"489_CR64","first-page":"169","volume-title":"Automated Deduction in Geometry, volume 6877 of Lecture Notes in Computer Science","author":"P Quaresma","year":"2011","unstructured":"Quaresma, P.: Thousands of geometric problems for geometric Theorem Provers (TGTP). In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry, volume 6877 of Lecture Notes in Computer Science, pp. 169\u2013181. Springer, New York (2011)"},{"key":"489_CR65","first-page":"221","volume-title":"Artificial Intelligence and Symbolic Computation, volume 11110 of Lecture Notes in Computer Science","author":"P Quaresma","year":"2018","unstructured":"Quaresma, P.: Automatic deduction in an AI geometry book. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) Artificial Intelligence and Symbolic Computation, volume 11110 of Lecture Notes in Computer Science, pp. 221\u2013226. Springer, New York (2018)"},{"key":"489_CR66","volume-title":"The Interactive Geometry Software Cinderella","author":"J Richter-Gebert","year":"1999","unstructured":"Richter-Gebert, J., Kortenkamp, U.: The Interactive Geometry Software Cinderella. Springer, New York (1999)"},{"key":"489_CR67","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1006135322108","volume":"23","author":"T Recio","year":"1999","unstructured":"Recio, T., V\u00e9lez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23, 63\u201382 (1999)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"489_CR68","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1564\/tme_v26.2.06","volume":"26","author":"V Santos","year":"2019","unstructured":"Santos, V., Baeta, N., Quaresma, P.: Geometrography in dynamic geometry. Int. J. Technol. Math. Educ. 26(2), 89\u201396 (2019)","journal-title":"Int. J. Technol. Math. Educ."},{"key":"489_CR69","unstructured":"Santiago, E., Hendriks, M., Kreis, Y., Kortenkamp, U., Marqu\u00e8s, D.: i2g Common File Format Final Version. Technical report D3.10, The Intergeo Consortium (2010)"},{"key":"489_CR70","first-page":"201","volume-title":"Automated Deduction in Geometry, Volume 6877 of Lecture Notes in Computer Science","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.) Automated Deduction in Geometry, Volume 6877 of Lecture Notes in Computer Science, vol. 6877, pp. 201\u2013220. Springer, Berlin (2011)"},{"key":"489_CR71","unstructured":"Stahl, R.J.: Using \u201cthink-time\u201d and \u201cwait-time\u201d skillfully in the classroom. Technical report, ERIC Digest (1994)"},{"key":"489_CR72","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"489_CR73","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Technical report, RAND Corporation (1951)","DOI":"10.1525\/9780520348097"},{"key":"489_CR74","doi-asserted-by":"crossref","unstructured":"van Dalen, D.: Logic and Structure. Universitext, Springer (1980)","DOI":"10.1007\/978-3-662-08402-1"},{"key":"489_CR75","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-7091-6604-8_8","volume-title":"Automated Pratical Reasoning","author":"D Wang","year":"1995","unstructured":"Wang, D.: Reasoning about geometric problems using an elimination method. In: Pfalzgraf, J., Wang, D. (eds.) Automated Pratical Reasoning, pp. 147\u2013185. Springer, New York (1995)"},{"key":"489_CR76","first-page":"240","volume-title":"Mathematical Software\u2014ICMS 2014, volume 8592 of Lecture Notes in Computer Science","author":"D Wang","year":"2014","unstructured":"Wang, D., Chen, X., An, W., Jiang, L., Song, D.: Opengeo: an open geometric knowledge base. In: Hong, H., Yap, C. (eds.) Mathematical Software\u2014ICMS 2014, volume 8592 of Lecture Notes in Computer Science, pp. 240\u2013245. Springer, Berlin (2014)"},{"key":"489_CR77","unstructured":"Wiedijk, F.: The de Bruijn factor. Poster at International Conference on Theorem Proving in Higher Order Logics (TPHOL2000), 2000. Portland, Oregon, USA, 14\u201318 August (2000)"},{"key":"489_CR78","doi-asserted-by":"crossref","unstructured":"Wu, W.-T.: On the decision problem and the mechanization of theorem proving in elementary geometry. In: Automated Theorem Proving: After 25 Years, Volume\u00a029 of Contemporary Mathematics, pp. 213\u2013234. American Mathematical Society (1984)","DOI":"10.1090\/conm\/029\/12"},{"issue":"3","key":"489_CR79","first-page":"43","volume":"14","author":"W-K Wong","year":"2011","unstructured":"Wong, W.-K., Yin, S.-K., Yang, H.-H., Cheng, Y.-H.: Using computer-assisted multiple representations in learning geometry proofs. Educ. Technol. Soc. 14(3), 43\u201354 (2011)","journal-title":"Educ. Technol. Soc."},{"key":"489_CR80","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10817-009-9162-5","volume":"45","author":"Z Ye","year":"2010","unstructured":"Ye, Z., Chou, S.-C., Gao, X.-S.: Visually dynamic presentation of proofs in plane geometry, part 1. J. Autom. Reason. 45, 213\u2013241 (2010)","journal-title":"J. Autom. Reason."},{"key":"489_CR81","first-page":"189","volume-title":"Automated Deduction in Geometry, Volume 6301 of Lecture Notes in Computer Science","author":"Z Ye","year":"2011","unstructured":"Ye, Z., Chou, S.-C., Gao, X.-S.: An introduction to Java geometry expert. In: Sturm, T., Zengler, C. (eds.) Automated Deduction in Geometry, Volume 6301 of Lecture Notes in Computer Science, pp. 189\u2013195. Springer, Berlin (2011)"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-020-00489-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11786-020-00489-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-020-00489-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,8]],"date-time":"2024-08-08T11:39:58Z","timestamp":1723117198000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11786-020-00489-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,25]]},"references-count":81,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["489"],"URL":"https:\/\/doi.org\/10.1007\/s11786-020-00489-7","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"type":"print","value":"1661-8270"},{"type":"electronic","value":"1661-8289"}],"subject":[],"published":{"date-parts":[[2020,6,25]]},"assertion":[{"value":"12 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 June 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}