{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:32:03Z","timestamp":1762324323959,"version":"3.41.0"},"reference-count":92,"publisher":"Springer Science and Business Media LLC","issue":"2-4","license":[{"start":{"date-parts":[[2018,9,6]],"date-time":"2018-09-06T00:00:00Z","timestamp":1536192000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/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"}]},{"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"}]},{"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":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s10472-018-9598-6","type":"journal-article","created":{"date-parts":[[2018,9,6]],"date-time":"2018-09-06T05:27:08Z","timestamp":1536211628000},"page":"119-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Portfolio theorem proving and prover runtime prediction for geometry"],"prefix":"10.1007","volume":"85","author":[{"given":"Mladen","family":"Nikoli\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0526-899X","authenticated-orcid":false,"given":"Vesna","family":"Marinkovi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zolt\u00e1n","family":"Kov\u00e1cs","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":[[2018,9,6]]},"reference":[{"key":"9598_CR1","doi-asserted-by":"crossref","unstructured":"Aigner, M., Biere, A., Kirsch, C.M., Niemetz, A., Preiner, M.: Analysis of portfolio-style parallel SAT solving on current multi-core architectures. In: Fourth Pragmatics of SAT workshop, a workshop of the SAT 2013 conference. POS-13, pp. 28\u201340 (2013)","DOI":"10.29007\/73n4"},{"issue":"2","key":"9598_CR2","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2014","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. 52(2), 191\u2013213 (2014)","journal-title":"J. Autom. Reason."},{"key":"9598_CR3","unstructured":"Aloul, F., Sierawski, B., Sakallah, K.: A tool for measuring progress of backtrack-search solvers. In: Theory and Applications of Satisfiability Testing - SAT 2002 (2002)"},{"issue":"4-5","key":"9598_CR4","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1017\/S1471068414000179","volume":"14","author":"R Amadini","year":"2014","unstructured":"Amadini, R., Gabbrielli, M., Mauro, J.: Sunny: a lazy portfolio approach for constraint solving. Theory Pract. Logic Program. 14(4-5), 509\u2013524 (2014)","journal-title":"Theory Pract. Logic Program."},{"key":"9598_CR5","doi-asserted-by":"crossref","unstructured":"Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M., Piette, C.: Revisiting clause exchange in parallel SAT solving. In: Theory and Applications of Satisfiability Testing \u2013 SAT 2012, pp. 200\u2013213. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31612-8_16"},{"key":"9598_CR6","doi-asserted-by":"crossref","unstructured":"Bartz-Beielstein, T., Lasarczyk, C.W.G., Preuss, M.: Sequential parameter optimization. In: 2005 IEEE Congress on Evolutionary Computation, vol. 1, pp. 773\u2013780 (2005)","DOI":"10.1109\/CEC.2005.1554761"},{"issue":"1","key":"9598_CR7","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."},{"issue":"1","key":"9598_CR8","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10817-015-9326-4","volume":"55","author":"F Botana","year":"2015","unstructured":"Botana, F., Hohenwarter, M., Jani\u010di\u0107, P., Kov\u00e1cs, Z., Petrovi\u0107, I., Recio, T., Weitzhofer, S.: Automated theorem proving in GeoGebra: current achievements. J. Autom. Reason. 55(1), 39\u201359 (2015)","journal-title":"J. Autom. Reason."},{"issue":"3-4","key":"9598_CR9","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/s10472-014-9438-2","volume":"74","author":"F Botana","year":"2015","unstructured":"Botana, F., Kov\u00e1cs, Z.: A singular web service for geometric computations. Ann. Math. Artif. Intell. 74(3-4), 359\u2013370 (2015)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9598_CR10","doi-asserted-by":"publisher","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":"9598_CR11","doi-asserted-by":"crossref","unstructured":"Chou, S.-C., Gao, X.-S.: Automated reasoning in geometry. In: Handbook of Automated Reasoning. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50013-8"},{"key":"9598_CR12","doi-asserted-by":"publisher","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)"},{"key":"9598_CR13","doi-asserted-by":"crossref","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: An introduction to geometry expert. In: CADE 13, Volume 1104 of Lecture Notes in Artificial Intelligence. Springer, Berlin (1996)","DOI":"10.1007\/3-540-61511-3_86"},{"key":"9598_CR14","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","volume":"61","author":"\u0141 Czajka","year":"2018","unstructured":"Czajka, \u0141., Kaliszyk, C.: Hammer for Coq automation for dependent type theory. J. Autom. Reason. 61, 423\u2013453 (2018)","journal-title":"J. Autom. Reason."},{"key":"9598_CR15","volume-title":"Pattern Classification","author":"R Duda","year":"2000","unstructured":"Duda, R., Hart, P., Stork, D.: Pattern Classification. Wiley-Interscience, New York (2000)"},{"key":"9598_CR16","unstructured":"Duncan, H., Bundy, A., Levine, J., Storkey, A., Pollet, M.: The use of data-mining for the automatic formation of tactics. In: Proceedings of the Workshop on Computer-Supported Mathematical Theory Development, IJCAR 2004 (2004)"},{"key":"9598_CR17","doi-asserted-by":"crossref","unstructured":"F\u00e4rber, M., Brown, C.: Internal guidance for Satallax. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning, pp. 349\u2013361. Springer International Publishing (2016)","DOI":"10.1007\/978-3-319-40229-1_24"},{"key":"9598_CR18","doi-asserted-by":"crossref","unstructured":"F\u00e4rber, M., Kaliszyk, C.: Random forests for premise selection. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems, pp. 325\u2013340. Springer International Publishing (2015)","DOI":"10.1007\/978-3-319-24246-0_20"},{"key":"9598_CR19","doi-asserted-by":"crossref","unstructured":"Fink, E.: How to solve it automatically: selection among problem-solving methods. In: Proceedings of the Fourth International Conference on Artificial Intelligence Planning Systems, pp. 128\u2013136. AAAI Press (1998)","DOI":"10.21236\/ADA327284"},{"key":"9598_CR20","doi-asserted-by":"crossref","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T., Schneider, M.T., Ziller, S.: A portfolio solver for answer set programming: preliminary report. In: Logic Programming and Nonmonotonic Reasoning, LPNMR 2011, pp. 352\u2013357. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-20895-9_40"},{"key":"9598_CR21","doi-asserted-by":"crossref","unstructured":"Gelernter, H.: Realisation of a geometry-proving machine. In: Automation of Reasoning. Springer, Berlin (1983)","DOI":"10.1007\/978-3-642-81952-0_8"},{"key":"9598_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-55864-1","volume-title":"Linear Regression","author":"J Gross","year":"2003","unstructured":"Gross, J.: Linear Regression. Springer, Berlin (2003)"},{"key":"9598_CR23","doi-asserted-by":"crossref","unstructured":"Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: Principles and Practice of Constraint Programming \u2013 CP 2010, pp. 252\u2013265. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-15396-9_22"},{"key":"9598_CR24","doi-asserted-by":"crossref","unstructured":"Haim, S., Walsh, T.: Online estimation of SAT solving runtime. In: Theory and Applications of Satisfiability Testing \u2013 SAT 2008, pp. 133\u2013138. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-79719-7_12"},{"key":"9598_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-21606-5","volume-title":"The Elements of Statistical Learning","author":"T Hastie","year":"2001","unstructured":"Hastie, T., Tibshirani, R., Friedman, J.: The Elements of Statistical Learning. Springer, New York (2001)"},{"key":"9598_CR26","unstructured":"Helmert, M., R\u00f6ger, G., Karpas, E.: Fast downward stone soup: a baseline for building planner portfolios. In: Proceedings of the ICAPS 2011 Workshop of AI Planning and Learning (2011)"},{"key":"9598_CR27","doi-asserted-by":"crossref","unstructured":"Ho, T.K.: Random decision forests. In: Proceedings of the Third International Conference on Document Analysis and Recognition (Volume 1), ICDAR \u201995, pp. 278\u2013282. IEEE Computer Society, Los Alamitos (1995)","DOI":"10.1109\/ICDAR.1995.598994"},{"key":"9598_CR28","volume-title":"GeoGebra: ein softwaresystem f\u00fcr dynamische geometrie und algebra der ebene. Master\u2019s Thesis, Paris Lodron University","author":"M Hohenwarter","year":"2002","unstructured":"Hohenwarter, M.: GeoGebra: ein softwaresystem f\u00fcr dynamische geometrie und algebra der ebene. Master\u2019s Thesis, Paris Lodron University. Salzburg, Austria (2002)"},{"key":"9598_CR29","doi-asserted-by":"crossref","unstructured":"Hurley, B., Kotthoff, L., Malitsky, L., O\u2019Sullivan, B.: Proteus: a hierarchical portfolio of solvers and transformations. In: Integration of AI and OR Techniques in Constraint Programming, CPAIOR 2014, pp. 301\u2013317. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07046-9_22"},{"key":"9598_CR30","unstructured":"Hurley, B., O\u2019Sullivan, B.: Statistical regimes and runtime prediction. In: Proceedings of the 24th International Conference on Artificial Intelligence, pp. 318\u2013324. AAAI Press (2015)"},{"key":"9598_CR31","doi-asserted-by":"crossref","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Learning and Intelligent Optimization, LION 5, pp. 507\u2013523. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-25566-3_40"},{"key":"9598_CR32","doi-asserted-by":"crossref","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Parallel algorithm configuration. In: Learning and Intelligent Optimization, LION 6, pp. 55\u201370. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-34413-8_5"},{"key":"9598_CR33","doi-asserted-by":"crossref","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K., Murphy, K.: Time-bounded sequential parameter optimization. In: Learning and Intelligent Optimization, LION 4, pp. 281\u2013298. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-13800-3_30"},{"key":"9598_CR34","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.artint.2013.10.003","volume":"206","author":"F Hutter","year":"2014","unstructured":"Hutter, F., Lin, X., Hoos, H.H., Leyton-Brown, K.: Algorithm runtime prediction: methods & evaluation. Artif. Intell. 206, 79\u2013111 (2014)","journal-title":"Artif. Intell."},{"key":"9598_CR35","doi-asserted-by":"crossref","unstructured":"Jakubuv, J., Urban, J.: Blistrtune: hierarchical invention of theorem proving strategies. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Cpp. 2017, pp. 43\u201352 (2017)","DOI":"10.1145\/3018610.3018619"},{"key":"9598_CR36","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P.: GCLC \u2013 a tool for constructive euclidean geometry and more than that. In: Proceedings of International Congress of Mathematical Software (ICMS 2006), Volume 4151 of Lecture Notes in Computer Science, pp. 58\u201373. Springer, Berlin (2006)","DOI":"10.1007\/11832225_6"},{"key":"9598_CR37","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P., Quaresma, P.: System description: GCLCprover + GeoThms. In: International Joint Conference on Automated Reasoning (IJCAR-2006), Volume 4130 of Lecture Notes in Artificial Intelligence, pp. 145\u2013150. Springer, Berlin (2006)","DOI":"10.1007\/11814771_13"},{"key":"9598_CR38","doi-asserted-by":"publisher","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, 489\u2013532 (2012)","journal-title":"J. Autom. Reason."},{"issue":"1-2","key":"9598_CR39","doi-asserted-by":"publisher","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. Reason. 44(1-2), 3\u201324 (2010)","journal-title":"J. Autom. Reason."},{"key":"9598_CR40","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P., Quaresma, P.: Automatic verification of regular constructions in dynamic geometry systems. In: Automated Deduction in Geometry, Volume 4869 of Lecture Notes in Artificial Intelligence, pp. 39\u201351. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-77356-6_3"},{"key":"9598_CR41","doi-asserted-by":"crossref","unstructured":"Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Algorithm selection and scheduling. In: Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming, CP\u201911, pp. 454\u2013469. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-23786-7_35"},{"key":"9598_CR42","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: Femalecop: fairly efficient machine learning connection prover. In: Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings, pp. 88\u201396 (2015)","DOI":"10.1007\/978-3-662-48899-7_7"},{"key":"9598_CR43","unstructured":"Kaliszyk, C., Urban, J., Vyskocil, J.: Efficient semantic features for automated reasoning over large theories. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 3084\u20133090 (2015)"},{"key":"9598_CR44","doi-asserted-by":"crossref","unstructured":"Komendantskaya, E., Heras, J., Grov, G.: Machine learning in proof general: interfacing interfaces. In: Proceedings 10th International Workshop on User Interfaces for Theorem Provers, UITP 2012, pp. 15\u201341 (2012)","DOI":"10.4204\/EPTCS.118.2"},{"issue":"3","key":"9598_CR45","doi-asserted-by":"crossref","first-page":"257","DOI":"10.3233\/AIC-2012-0533","volume":"25","author":"L Kotthoff","year":"2012","unstructured":"Kotthoff, L., Gent, I.P., Miguel, I.: An evaluation of machine learning in algorithm selection for search problems. AI Commun. 25(3), 257\u2013270 (2012)","journal-title":"AI Commun."},{"key":"9598_CR46","volume-title":"Computer Based Conjectures and Proofs in Teaching Euclidean Geometry. PhD Thesis Computer Based Johannes Kepler University","author":"Z Kov\u00e1cs","year":"2015","unstructured":"Kov\u00e1cs, Z.: Computer Based Conjectures and Proofs in Teaching Euclidean Geometry. PhD Thesis Computer Based Johannes Kepler University. Linz, Austria (2015)"},{"key":"9598_CR47","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, Z., Parisse, B.: Giac and GeoGebra \u2013 improved Gr\u00f6bner basis computations. In: Computer Algebra and Polynomials, Lecture Notes in Computer Science, pp. 126\u2013138. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-15081-9_7"},{"key":"9598_CR48","unstructured":"Kov\u00e1cs, Z., Recio, T., Weitzhofer, S.: Implementing theorem proving in GeoGebra by using exact check of a statement in a bounded number of test cases. In: Proceedings EACA 2012 Libro de res\u00famenes del XIII Encuentro de \u00c1lgebra Computacional y Aplicaciones, pp. 123\u2013126. Universidad de Alcal\u00e1 (2012)"},{"issue":"1","key":"9598_CR49","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/1758-2946-6-1","volume":"6","author":"D Krstaji\u0107","year":"2014","unstructured":"Krstaji\u0107, D., Buturovi\u0107, L.J., Leahy, D.E., Thomas, S.: Cross-validation pitfalls when selecting and assessing regression and classification models. J. Cheminf. 6(1), 1\u201315 (2014)","journal-title":"J. Cheminf."},{"issue":"2","key":"9598_CR50","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10817-015-9329-1","volume":"55","author":"D K\u00fchlwein","year":"2015","unstructured":"K\u00fchlwein, D., Urban, J.: Males: A framework for automatic tuning of automated theorem provers. J. Autom. Reason. 55(2), 91\u2013116 (2015)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9598_CR51","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1214\/aoms\/1177729694","volume":"22","author":"S Kullback","year":"1951","unstructured":"Kullback, S., Leibler, R.: On information and sufficiency. Ann. Math. Stat. 22(1), 79\u201386 (1951)","journal-title":"Ann. Math. Stat."},{"key":"9598_CR52","doi-asserted-by":"crossref","unstructured":"Lindauer, M., Hoos, H., Hutter, F.: From sequential algorithm selection to parallel portfolio selection. In: Learning and Intelligent Optimization, LION 9, pp. 1\u201316. Springer International Publishing (2015)","DOI":"10.1007\/978-3-319-19084-6_1"},{"key":"9598_CR53","unstructured":"Lobjois, L., Lema\u00eetre, M.: Branch and bound algorithm selection by performance prediction. In: Proceedings of the Fifteenth National\/Tenth Conference on Artificial Intelligence\/Innovative Applications of Artificial Intelligence, AAAI\u201998\/IAAI\u201998, pp. 353\u2013358. American Association for Artificial Intelligence (1998)"},{"key":"9598_CR54","doi-asserted-by":"crossref","unstructured":"Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Non-model-based algorithm portfolios for SAT. In: Theory and Applications of Satisfiability Testing, SAT 2011 (2011)","DOI":"10.1007\/978-3-642-21581-0_33"},{"key":"9598_CR55","doi-asserted-by":"crossref","unstructured":"Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Parallel SAT solver selection and scheduling. In: Principles and Practice of Constraint Programming, CP 2012, pp. 512\u2013526. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-33558-7_38"},{"key":"9598_CR56","doi-asserted-by":"crossref","unstructured":"Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Boosting sequential solver portfolios: knowledge sharing and accuracy prediction. In: Learning and Intelligent Optimization, LION 7, pp. 153\u2013167. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-44973-4_17"},{"key":"9598_CR57","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: Proceedings First Workshop on CTP Components for Educational Software, Volume 79 of Electronic Proceedings in Theoretical Computer Science, pp. 63\u201381. Open Publishing Association (2012)","DOI":"10.4204\/EPTCS.79.4"},{"issue":"1","key":"9598_CR58","first-page":"29","volume":"XVIII","author":"V Marinkovi\u0107","year":"2015","unstructured":"Marinkovi\u0107, V.: On-line compendium of triangle construction problems with automatically generated solutions. The Teaching of Mathematics XVIII(1), 29\u201344 (2015)","journal-title":"The Teaching of Mathematics"},{"issue":"2","key":"9598_CR59","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1080\/0952813X.2015.1132271","volume":"29","author":"V Marinkovi\u0107","year":"2017","unstructured":"Marinkovi\u0107, V.: ArgoTriCS \u2013 automated triangle construction solver. J. Exp. Theor. Artif. Intell. 29(2), 247\u2013271 (2017)","journal-title":"J. Exp. Theor. Artif. Intell."},{"key":"9598_CR60","doi-asserted-by":"crossref","unstructured":"Marinkovi\u0107, V., Jani\u010di\u0107, P.: Towards understanding triangle construction problems. In: Intelligent Computer Mathematics - CICM 2012, Volume 7362 of Lecture Notes in Computer Science. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31374-5_9"},{"key":"9598_CR61","unstructured":"Marinkovi\u0107, V., Jani\u010di\u0107, P., Schreck, P.: Solving geometric construction problems supported by theorem proving. In: Proceedings of the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), pp. 121\u2013146. CISUC Technical report TR 2014\/01, University of Coimbra (2014)"},{"key":"9598_CR62","doi-asserted-by":"crossref","unstructured":"Menouer, T., Baarir, S.: Parallel learning portfolio-based solvers. In: International Conference on Computational Science, ICCS 2017, volume 108 (2017)","DOI":"10.1016\/j.procs.2017.05.140"},{"key":"9598_CR63","volume-title":"Machine learning: a probabilistic perspective","author":"KP Murphy","year":"2012","unstructured":"Murphy, K.P.: Machine learning: a probabilistic perspective. MIT Press, Cambridge (2012)"},{"key":"9598_CR64","doi-asserted-by":"crossref","unstructured":"Nikoli\u0107, M., Mari\u0107, F., Jani\u010di\u0107, P.: Instance-based selection of policies for SAT solvers. In: Theory and Applications of Satisfiability Testing - SAT 2009, Volume 5584 of Lecture Notes in Computer Science, pp. 326\u2013340. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02777-2_31"},{"key":"9598_CR65","unstructured":"Nikoli\u0107, M., Mari\u0107, F., Jani\u010di\u0107, P.: Simple algorithm portfolio for SAT. Artif. Intell. Rev., pp. 1\u20139 (2012)"},{"key":"9598_CR66","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, Volume 2283 of Lecture Notes in Computer Science. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9598_CR67","doi-asserted-by":"crossref","unstructured":"Nudelman, E., Leyton-Brown, K., Hoos, H.H., Devkar, A., Shoham, Y.: Understanding random SAT: beyond the clauses-to-variables ratio. In: Principles and Practice of Constraint Programming \u2013 CP 2004, pp. 438\u2013452. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30201-8_33"},{"key":"9598_CR68","unstructured":"O\u2019Mahony, E., Hebrard, E., Holland, A., Nugent, C.: Using case-based reasoning in an algorithm portfolio for constraint solving. In: Irish Conference on Artificial Intelligence and Cognitive Science (2008)"},{"key":"9598_CR69","unstructured":"Paulson, L.C.: The Isabelle reference manual (2006)"},{"key":"9598_CR70","volume-title":"Introducing Dynamic Mathematics Software to Mathematics Teachers: The Case of GeoGebra. PhD Thesis, Paris Lodron University","author":"J Preiner","year":"2008","unstructured":"Preiner, J.: Introducing Dynamic Mathematics Software to Mathematics Teachers: The Case of GeoGebra. PhD Thesis, Paris Lodron University. Salzburg, Austria (2008)"},{"key":"9598_CR71","doi-asserted-by":"crossref","unstructured":"Pulina, L., Tacchella, A.: A multi-engine solver for quantified boolean formulas. In: Principles and Practice of Constraint Programming \u2013 CP 2007, pp. 574\u2013589. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-74970-7_41"},{"issue":"1","key":"9598_CR72","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/s10601-008-9051-2","volume":"14","author":"L Pulina","year":"2009","unstructured":"Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified boolean formulas. Constraints 14(1), 80\u2013116 (2009)","journal-title":"Constraints"},{"key":"9598_CR73","volume-title":"Linear Statistical Inference and its Applications","author":"C Radhakrishna Rao","year":"1973","unstructured":"Radhakrishna Rao, C.: Linear Statistical Inference and its Applications. Wiley, New York (1973)"},{"issue":"2-3","key":"9598_CR74","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":"9598_CR75","doi-asserted-by":"crossref","unstructured":"Rizzini, M., Fawcett, C., Vallati, M., Gerevini, A.E., Hoos, H.H.: Static and dynamic portfolio methods for optimal planning: an empirical analysis. Int. J. Artif. Intell. Tools 26(01) (2017)","DOI":"10.1142\/S0218213017600065"},{"issue":"5","key":"9598_CR76","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1016\/j.artint.2008.11.009","volume":"173","author":"M Roberts","year":"2009","unstructured":"Roberts, M., Howe, A.: Learning from planner performance. Artif. Intell. 173 (5), 536\u2013561 (2009)","journal-title":"Artif. Intell."},{"key":"9598_CR77","unstructured":"Samulowitz, H., Memisevic, R.: Learning to solve QBF. In: Proceedings of the 22Nd National Conference on Artificial Intelligence, AAAI \u201907, pp. 255\u2013260. AAAI Press (2007)"},{"key":"9598_CR78","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2,3) (2002)"},{"key":"9598_CR79","doi-asserted-by":"crossref","unstructured":"Seipp, J., Sievers, S., Helmert, M., Hutter, F.: Automatic configuration of sequential planning portfolios. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence AAAI\u201915, pp. 3364\u20133370 AAAI Press (2015)","DOI":"10.1609\/aaai.v29i1.9640"},{"key":"9598_CR80","doi-asserted-by":"crossref","unstructured":"Sonobe, T., Kondoh, S., Inaba, M.: Community branching for parallel portfolio SAT solvers. In: Theory and Applications of Satisfiability Testing \u2013 SAT 2014, pp. 188\u2013196, Cham. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-09284-3_14"},{"issue":"4","key":"9598_CR81","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/s10601-014-9165-7","volume":"19","author":"M Stojadinovi\u0107","year":"2014","unstructured":"Stojadinovi\u0107, M., Mari\u0107, F.: meSAT: multiple encodings of CSP to SAT. Constraints 19(4), 380\u2013403 (2014)","journal-title":"Constraints"},{"issue":"3\u20134","key":"9598_CR82","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s10472-014-9443-5","volume":"74","author":"SS \u00d0u\u0111evi\u0107","year":"2015","unstructured":"\u00d0u\u0111evi\u0107, S.S., Narboux, J., Jani\u010di\u0107, P.: Automated generation of machine verifiable and readable proofs: A case study of Tarski\u2019s geometry. Ann. Math. Artif. Intell. 74(3\u20134), 249\u2013269 (2015)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9598_CR83","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: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry, Volume 6877 of Lecture Notes in Computer Science, Springer (2011)","DOI":"10.1007\/978-3-642-25070-5_12"},{"key":"9598_CR84","unstructured":"The Coq development team. The Coq proof assistant reference manual, Version 8.7.2. r 2 Project (2018)"},{"key":"9598_CR85","unstructured":"Trgalova, J., Kortenkamp, U., Jahn, A.P., Libbrecht, P., Mercat, C., Recio, T.: Sophie Soury-Lavergne I2GEO.NET. Seventh Congress of the European Society for Research in Mathematics Education, Rzeszow, Poland, pp. 2986\u20132987. https:\/\/hal.archives-ouvertes.fr\/hal-01045138 (2011)"},{"key":"9598_CR86","unstructured":"Urban, J.: Blistr: the blind strategymaker. In: Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015, pp. 312\u2013319 (2015)"},{"key":"9598_CR87","doi-asserted-by":"crossref","unstructured":"Urban, J., Vysko\u010dil, J., \u0160t\u011bp\u00e1nek, P.: Malecop machine learning connection prover. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods, pp. 263\u2013277. Springer (2011)","DOI":"10.1007\/978-3-642-22119-4_21"},{"key":"9598_CR88","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10732-017-9328-y","volume":"24","author":"M Wagner","year":"2017","unstructured":"Wagner, M., Lindauer, M., M\u0131s\u0131r, M., Nallaperuma, S., Hutter, F.: A case study of algorithm selection for the traveling thief problem. J. Heuristics 24, 295\u2013320 (2017)","journal-title":"J. Heuristics"},{"key":"9598_CR89","doi-asserted-by":"crossref","unstructured":"Wang, D.: Geother 1.1: handling and proving geometric theorems automatically. In: Automated Deduction in Geometry, Volume 2930 of Lecture Notes in Artificial Intelligence, pp. 194\u2013215. Springer (2004)","DOI":"10.1007\/978-3-540-24616-9_12"},{"key":"9598_CR90","doi-asserted-by":"publisher","first-page":"57","DOI":"10.4204\/EPTCS.118.4","volume":"118","author":"M Wenzel","year":"2013","unstructured":"Wenzel, M.: READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking. Electronic Proceedings in Theoretical Computer Science 118, 57\u201371 (2013)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"4","key":"9598_CR91","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1080\/0025570X.1985.11976988","volume":"55","author":"W Wernick","year":"1982","unstructured":"Wernick, W.: Triangle constructions with three located points. Math. Mag. 55 (4), 227\u2013230 (1982)","journal-title":"Math. Mag."},{"key":"9598_CR92","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"X Lin","year":"2008","unstructured":"Lin, X., Hutter, F., Hoss, H.H., Leyton-Brown, K.: SATzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565\u2013606 (2008)","journal-title":"J. Artif. Intell. Res."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-018-9598-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-018-9598-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-018-9598-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T22:39:15Z","timestamp":1751841555000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-018-9598-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,6]]},"references-count":92,"journal-issue":{"issue":"2-4","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["9598"],"URL":"https:\/\/doi.org\/10.1007\/s10472-018-9598-6","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2018,9,6]]},"assertion":[{"value":"6 September 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}