{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:44:48Z","timestamp":1762325088429,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030860585"},{"type":"electronic","value":"9783030860592"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-86059-2_16","type":"book-chapter","created":{"date-parts":[[2021,8,31]],"date-time":"2021-08-31T17:48:17Z","timestamp":1630432097000},"page":"266-278","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Learning Theorem Proving Components"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0541-3889","authenticated-orcid":false,"given":"Karel","family":"Chvalovsk\u00fd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8848-5537","authenticated-orcid":false,"given":"Jan","family":"Jakub\u016fv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9361-1921","authenticated-orcid":false,"given":"Miroslav","family":"Ol\u0161\u00e1k","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1384-1613","authenticated-orcid":false,"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,30]]},"reference":[{"issue":"3","key":"16_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reasoning 44(3), 175\u2013205 (2010)","journal-title":"J. Autom. Reasoning"},{"issue":"2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2013","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 (2013). https:\/\/doi.org\/10.1007\/s10817-013-9286-5","journal-title":"J. Autom. Reason."},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Bezdek, J.C., Ehrlich, R., Full, W.: FCM: the fuzzy c-means clustering algorithm. Comput. Geosci. 10(2), 191\u2013203 (1984). https:\/\/doi.org\/10.1016\/0098-3004(84)90020-7. https:\/\/www.sciencedirect.com\/science\/article\/pii\/0098300484900207","DOI":"10.1016\/0098-3004(84)90020-7"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reason. 9(1), 101\u2013148 (2016). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4593. http:\/\/dx.doi.org\/10.6092\/issn.1972-5787\/4593","DOI":"10.6092\/issn.1972-5787\/4593"},{"issue":"10","key":"16_CR5","doi-asserted-by":"publisher","first-page":"P10008","DOI":"10.1088\/1742-5468\/2008\/10\/P10008","volume":"2008","author":"VD Blondel","year":"2008","unstructured":"Blondel, V.D., Guillaume, J.L., Lambiotte, R., Lefebvre, E.: Fast unfolding of communities in large networks. J. Stat. Mech: Theory Exp. 2008(10), P10008 (2008)","journal-title":"J. Stat. Mech: Theory Exp."},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-030-29436-6_12","volume-title":"Automated Deduction \u2013 CADE 27","author":"K Chvalovsk\u00fd","year":"2019","unstructured":"Chvalovsk\u00fd, K., Jakub\u016fv, J., Suda, M., Urban, J.: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 197\u2013215. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_12"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Dias, M.L.D.: fuzzy-c-means: an implementation of fuzzy $$c$$-means clustering algorithm. (2019). https:\/\/doi.org\/10.5281\/zenodo.3066222. https:\/\/git.io\/fuzzy-c-means","DOI":"10.5281\/zenodo.3066222"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-18638-7_6","volume-title":"Graph Drawing Software","author":"J Ellson","year":"2004","unstructured":"Ellson, J., Gansner, E.R., Koutsofios, E., North, S.C., Woodhull, G.: Graphviz and dynagraph - static and dynamic graph drawing tools. In: J\u00fcnger, M., Mutzel, P. (eds.) Graph Drawing Software, pp. 127\u2013148. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-642-18638-7_6"},{"key":"16_CR9","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J.: TacticToe: learning to reason with HOL4 tactics. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7\u201312 May 2017. EPiC Series in Computing, vol. 46, pp. 125\u2013143. EasyChair (2017). http:\/\/www.easychair.org\/publications\/paper\/340355"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Gittins, J.C.: Bandit processes and dynamic allocation indices. J. Roy. Stat. Soc. Ser. B (Methodol.) 148\u2013177 (1979)","DOI":"10.1111\/j.2517-6161.1979.tb01068.x"},{"key":"16_CR11","unstructured":"Gottlob, G., Sutcliffe, G., Voronkov, A. (eds.): Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, 16\u201319 October 2015. EPiC Series in Computing, vol. 36. EasyChair (2015). http:\/\/www.easychair.org\/publications\/volume\/GCAI_2015"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/978-3-030-51054-1_29","volume-title":"Automated Reasoning","author":"J Jakub\u016fv","year":"2020","unstructured":"Jakub\u016fv, J., Chvalovsk\u00fd, K., Ol\u0161\u00e1k, M., Piotrowski, B., Suda, M., Urban, J.: ENIGMA anonymous: symbol-independent inference guiding machine (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 448\u2013463. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_29"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-319-42547-4_11","volume-title":"Intelligent Computer Mathematics","author":"J Jakub\u016fv","year":"2016","unstructured":"Jakub\u016fv, J., Urban, J.: Extending E prover with similarity based clause selection strategies. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 151\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-42547-4_11"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-62075-6_20","volume-title":"Intelligent Computer Mathematics","author":"J Jakub\u016fv","year":"2017","unstructured":"Jakub\u016fv, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 292\u2013302. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_20"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Jakub\u016fv, J., Urban, J.: Hierarchical invention of theorem proving strategies. AI Commun. 31(3), 237\u2013250 (2018). https:\/\/doi.org\/10.3233\/AIC-180761","DOI":"10.3233\/AIC-180761"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Jakub\u016fv, J., Urban, J.: Hammering Mizar by learning clause guidance. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, 9\u201312 September 2019, Portland, OR, USA. LIPIcs, vol. 141, pp. 34:1\u201334:8. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.34","DOI":"10.4230\/LIPIcs.ITP.2019.34"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reason. 55(3), 245\u2013256 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9330-8","DOI":"10.1007\/s10817-015-9330-8"},{"key":"16_CR18","unstructured":"Kaliszyk, C., Urban, J., Michalewski, H., s\u00e1k, M.O.: Reinforcement learning of theorem proving. In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3\u20138 December 2018, Montr\u00e9al, Canada, pp. 8836\u20138847 (2018). http:\/\/papers.nips.cc\/paper\/8098-reinforcement-learning-of-theorem-proving"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-36675-8_8","volume-title":"Automated Reasoning and Mathematics","author":"M Kinyon","year":"2013","unstructured":"Kinyon, M., Veroff, R., Vojt\u011bchovsk\u00fd, P.: Loops with abelian inner mapping groups: an application of automated deduction. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 151\u2013164. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36675-8_8"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/3-540-52885-7_131","volume-title":"10th International Conference on Automated Deduction","author":"W McCune","year":"1990","unstructured":"McCune, W.: Otter 2.0. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 663\u2013664. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_131"},{"key":"16_CR22","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11856290_4","volume-title":"Artificial Intelligence and Symbolic Computation","author":"W McCune","year":"2006","unstructured":"McCune, W.: Semantic guidance for saturation provers. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol. 4120, pp. 18\u201324. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11856290_4"},{"key":"16_CR24","unstructured":"McCune, W.: Otter 3.3 reference manual. Technical report ANL\/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003)"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Ol\u0161\u00e1k, M., Kaliszyk, C., Urban, J.: Property invariant embedding for automated reasoning. In: Giacomo, G.D., et al. (eds.) ECAI 2020\u201324th European Conference on Artificial Intelligence, 29 August\u20138 September 2020, Santiago de Compostela, Spain, 29 August\u20138 September 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020). Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 1395\u20131402. IOS Press (2020). https:\/\/doi.org\/10.3233\/FAIA200244","DOI":"10.3233\/FAIA200244"},{"issue":"1\u20132","key":"16_CR26","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1\u20132), 139\u2013161 (2003)","journal-title":"J. Symb. Comput."},{"key":"16_CR27","unstructured":"Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers (1992)"},{"key":"16_CR28","unstructured":"Raths, T., Otten, J.: randocop: randomizing the proof search order in the connection calculus. In: Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning, Sydney, Australia, 10\u201311 August 2008. CEUR Workshop Proceedings, vol. 373. CEUR-WS.org (2008). http:\/\/ceur-ws.org\/Vol-373\/paper-08.pdf"},{"key":"16_CR29","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)"},{"key":"16_CR30","unstructured":"Sch\u00e4fer, S., Schulz, S.: Breeding theorem proving heuristics with genetic algorithms. In: Gottlob et al. [11], pp. 263\u2013274. http:\/\/www.easychair.org\/publications\/paper\/Breeding_Theorem_Proving_Heuristics_with_Genetic_Algorithms"},{"issue":"2\u20133","key":"16_CR31","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"16_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49"},{"issue":"1\u20132","key":"16_CR33","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reasoning 37(1\u20132), 21\u201343 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"16_CR34","unstructured":"Urban, J.: BliStr: the blind strategymaker. In: Gottlob et al. [11], pp. 312\u2013319. http:\/\/www.easychair.org\/publications\/paper\/BliStr_The_Blind_Strategymaker"},{"issue":"3","key":"16_CR35","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R Veroff","year":"1996","unstructured":"Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: case studies. J. Autom. Reason. 16(3), 223\u2013239 (1996)","journal-title":"J. Autom. Reason."},{"key":"16_CR36","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1038\/s41592-019-0686-2","volume":"17","author":"P Virtanen","year":"2020","unstructured":"Virtanen, P., et al.: SciPy 1.0 contributors: SciPy 1.0: fundamental algorithms for scientific computing in python. Nat. Methods 17, 261\u2013272 (2020). https:\/\/doi.org\/10.1038\/s41592-019-0686-2","journal-title":"Nat. Methods"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-86059-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,31]],"date-time":"2021-08-31T17:56:03Z","timestamp":1630432563000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-86059-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030860585","9783030860592"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-86059-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"30 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Birmingham","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tableaux2021.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}