{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:07:16Z","timestamp":1784844436459,"version":"3.55.0"},"publisher-location":"Cham","reference-count":167,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031617157","type":"print"},{"value":"9783031617164","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-61716-4_4","type":"book-chapter","created":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:47:52Z","timestamp":1716954472000},"page":"54-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Learning Guided Automated Reasoning: A Brief Survey"],"prefix":"10.1007","author":[{"given":"Lasse","family":"Blaauwbroek","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David M.","family":"Cerna","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thibault","family":"Gauthier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"Jakub\u016fv","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,5,22]]},"reference":[{"issue":"2","key":"4_CR1","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 math by corpus analysis and kernel methods. JAR 52(2), 191\u2013213 (2014)","journal-title":"JAR"},{"key":"4_CR2","unstructured":"Alemi, A.A., Chollet, F., E\u00e9n, N., Irving, G., Szegedy, C., Urban, J.: DeepMath - deep sequence models for premise selection. In: NIPS 2016, pp. 2235\u20132243 (2016)"},{"key":"4_CR3","unstructured":"Allamanis, M., Chanthirasegaran, P., Kohli, P., Sutton, C.: Learning continuous semantic representations of symbolic expressions. In: ICML 2017, volume\u00a070 of Proceedings of Machine Learning Research, pp. 80\u201388. PMLR (2017)"},{"key":"4_CR4","unstructured":"Ayg\u00fcn, E., et al.: Proving theorems using incremental learning and hindsight experience replay. In: ICML 2022, vol. 162, pp. 1198\u20131210 (2022)"},{"key":"4_CR5","unstructured":"Balunovic, M.,\u00a0Bielik, P., Vechev, M.T.: Learning to solve SMT formulas. In: NeurIPS, pp. 10338\u201310349 (2018)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-20615-8_17","volume-title":"Intelligent Computer Mathematics","author":"G Bancerek","year":"2015","unstructured":"Bancerek, G., et al.: Mizar: state-of-the-art and Beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science(), vol. 9150, pp. 261\u2013279. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_17"},{"key":"4_CR7","unstructured":"Bansal, K., Loos, S., Rabe, M., Szegedy, C., Wilcox, S.: Holist: an environment for machine learning of higher order logic theorem proving. In: ICML 2019, vol.\u00a097, pp. 454\u2013463. PMLR (2019)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-030-79876-5_30","volume-title":"Automated Deduction - CADE 28","author":"F B\u00e1rtek","year":"2021","unstructured":"B\u00e1rtek, F., Suda, M.: Neural precedence recommender. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28. Lecture Notes in Computer Science(), vol. 12699, pp. 525\u2013542. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_30"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"B\u00e1rtek, F.,\u00a0Suda, M.: How much should this symbol weigh? A GNN-advised clause selection. In: LPAR 2023, vol.\u00a094 of EPiC, pp. 96\u2013111. EasyChair (2023)","DOI":"10.29007\/5f4r"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-030-53518-6_17","volume-title":"Intelligent Computer Mathematics","author":"L Blaauwbroek","year":"2020","unstructured":"Blaauwbroek, L., Urban, J., Geuvers, H.: The tactician - a seamless, interactive tactic learner and prover for Coq. In: Benzmuller, C., Miller, B. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science(), vol. 12236, pp. 271\u2013277. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_17"},{"issue":"1","key":"4_CR12","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101\u2013148 (2016)","journal-title":"J. Formalized Reasoning"},{"key":"4_CR13","unstructured":"Blanchette, J.C., El Ouraoui, D., Fontaine, P., Kaliszyk, C.: Machine learning for instance selection in SMT solving. In: AITP 2019 - 4th Conference on Artificial Intelligence and Theorem Proving, Obergurgl, Austria (2019)"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0004-3702(72)90041-0","volume":"3","author":"WW Bledsoe","year":"1972","unstructured":"Bledsoe, W.W., Boyer, R.S., Henneman, W.H.: Computer proofs of limit theorems. Artif. Intell. 3, 27\u201360 (1972)","journal-title":"Artif. Intell."},{"key":"4_CR15","unstructured":"Carlson, A.,\u00a0Cumby, C.,\u00a0Rosen, J.,\u00a0Roth, D.: The SNoW learning architecture, vol. 5. Technical report. UIUCDCS-R-99-2101, UIUC Computer Science Department (1999)"},{"key":"4_CR16","unstructured":"Chang, O., Flokas, L., Lipson, H., Spranger, M.: Assessing SATNet\u2019s ability to solve the symbol grounding problem. In: NeurIPS 2020, vol.\u00a033, pp. 1428\u20131439 (2020)"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Chen, T., Guestrin, C.: XGBoost: a scalable tree boosting system. In: Knowledge Discovery and Data Mining 2016, pp. 785\u2013794. ACM (2016)","DOI":"10.1145\/2939672.2939785"},{"key":"4_CR18","unstructured":"Chvalovsk\u00fd, K.: Top-down neural model for formulae. In: ICLR 2019. OpenReview.net (2019)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-030-86059-2_16","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"K Chvalovsk\u00fd","year":"2021","unstructured":"Chvalovsk\u00fd, K., Jakub\u016fv, J., Ols\u00e1k, M., Urban, J.: Learning theorem proving components. In: Das, A., Negri, S. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science(), vol. 12842, pp. 266\u2013278. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_16"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-030-29436-6_12","volume-title":"Automated Deduction - 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.) Automated Deduction - CADE 27. Lecture Notes in Computer Science(), vol. 11716, pp. 197\u2013215. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_12"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Chvalovsk\u00fd, K.,\u00a0Korovin, K.,\u00a0Piepenbrock, J.,\u00a0Urban, J.: Guiding an instantiation prover with graph neural networks. In: LPAR 2023, volume\u00a094 of EPiC Series in Computing, pp. 112\u2013123. EasyChair (2023)","DOI":"10.29007\/tp23"},{"key":"4_CR22","unstructured":"Colton, S., Bundy, A., Walsh, T.: Automatic concept formation in pure mathematics. In: IJCAI, pp. 786\u2013793. Morgan Kaufmann (1999)"},{"key":"4_CR23","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1613\/jair.1.13507","volume":"74","author":"A Cropper","year":"2022","unstructured":"Cropper, A., Dumancic, S.: Inductive logic programming at 30: a new introduction. J. Artif. Intell. Res. 74, 765\u2013850 (2022)","journal-title":"J. Artif. Intell. Res."},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Crouse, M., et al.: A deep reinforcement learning approach to first-order logic theorem proving. In: AAAI 2021, pp. 6279\u20136287 (2021)","DOI":"10.1609\/aaai.v35i7.16780"},{"key":"4_CR25","unstructured":"Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the MIZAR Mathematical Library. In: International Workshop on First-Order Theorem Proving (FTP\u201997), pp. 58\u201362 (1997)"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/B978-044450813-3\/50003-5","volume":"1","author":"M Davis","year":"2001","unstructured":"Davis, M.: The early history of automated deduction. Handb. Autom. Reasoning 1, 3\u201315 (2001)","journal-title":"Handb. Autom. Reasoning"},{"issue":"3","key":"4_CR27","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM (JACM) 7(3), 201\u2013215 (1960)","journal-title":"J. ACM (JACM)"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"LM de Moura","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"6","key":"4_CR29","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1002\/(SICI)1097-4571(199009)41:6<391::AID-ASI1>3.0.CO;2-9","volume":"41","author":"SC Deerwester","year":"1990","unstructured":"Deerwester, S.C., Dumais, S.T., Landauer, T.K., Furnas, G.W., Harshman, R.A.: Indexing by latent semantic analysis. JASIS 41(6), 391\u2013407 (1990)","journal-title":"JASIS"},{"key":"4_CR30","unstructured":"Denzinger, J.,\u00a0Fuchs, M.,\u00a0Goller, C.,\u00a0Schulz, S.: Learning from previous proof experience. Technical Report AR99-4, Institut f\u00fcr Informatik, TUM (1999)"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Denzinger, J.,\u00a0Schulz, S.: Learning domain knowledge to improve theorem proving. In: CADE 13, number 1104 in LNAI, pp. 62\u201376 (1996)","DOI":"10.1007\/3-540-61511-3_69"},{"key":"4_CR32","unstructured":"El\u00a0Ouraoui, D.: M\u00e9thodes pour le raisonnement d\u2019ordre sup\u00e9rieur dans SMT, Chapter 5. PhD thesis, Universit\u00e9 de Lorraine (2021)"},{"key":"4_CR33","doi-asserted-by":"publisher","first-page":"103521","DOI":"10.1016\/j.artint.2021.103521","volume":"299","author":"R Evans","year":"2021","unstructured":"Evans, R., et al.: Making sense of raw input. Artif. Intell. 299, 103521 (2021)","journal-title":"Artif. Intell."},{"key":"4_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1613\/jair.5714","volume":"61","author":"R Evans","year":"2018","unstructured":"Evans, R., Grefenstette, E.: Learning explanatory rules from noisy data. J. Artif. Intell. Res. 61, 1\u201364 (2018)","journal-title":"J. Artif. Intell. Res."},{"key":"4_CR35","unstructured":"Evans, R.,\u00a0Saxton, D.,\u00a0Amos, D.,\u00a0Kohli, P.,\u00a0Grefenstette, E.: Can neural networks understand logical entailment? In: ICLR 2018. OpenReview.net (2018)"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-24246-0_20","volume-title":"Frontiers of Combining Systems","author":"M F\u00e4rber","year":"2015","unstructured":"F\u00e4rber, M., Kaliszyk, C.: Random forests for premise selection. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems. Lecture Notes in Computer Science(), vol. 9322, pp. 325\u2013340. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_20"},{"issue":"2","key":"4_CR37","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/s10817-020-09576-7","volume":"65","author":"M F\u00e4rber","year":"2021","unstructured":"F\u00e4rber, M., Kaliszyk, C., Urban, J.: Machine learning guidance for connection tableaux. J. Autom. Reason. 65(2), 287\u2013320 (2021)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"4_CR38","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1017\/S1471068414000076","volume":"15","author":"D Fierens","year":"2015","unstructured":"Fierens, D., et al.: Inference and learning in probabilistic logic programs using weighted Boolean formulas. Theory Pract. Log. Prog. 15(3), 358\u2013401 (2015)","journal-title":"Theory Pract. Log. Prog."},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"First, E., Brun, Y.: Diversity-driven automated formal verification. In: Proceedings of the 44th International Conference on Software Engineering, ICSE \u201922, New York, NY, USA, pp. 749-761. Association for Computing Machinery (2022)","DOI":"10.1145\/3510003.3510138"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"First, E., Brun, Y., Guha, A.: TacTok: semantics-aware proof synthesis. Proc. ACM Program. Lang. 4(OOPSLA) (2020)","DOI":"10.1145\/3428299"},{"key":"4_CR41","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jsc.2018.04.005","volume":"90","author":"T Gauthier","year":"2019","unstructured":"Gauthier, T., Kaliszyk, C.: Aligning concepts across proof assistant libraries. J. Symb. Comput. 90, 89\u2013123 (2019)","journal-title":"J. Symb. Comput."},{"key":"4_CR42","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J.: Initial experiments with statistical conjecturing over large formal corpora. In: WIP@CIKM\u201916, volume 1785 of CEUR, pp. 219\u2013228 (2016)"},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"Gauthier, T.,\u00a0Kaliszyk, C.,\u00a0Urban, J.: TacticToe: learning to reason with HOL4 tactics. In: LPAR-21, pp. 125\u2013143 (2017)","DOI":"10.29007\/ntlb"},{"issue":"2","key":"4_CR44","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10817-020-09580-x","volume":"65","author":"T Gauthier","year":"2021","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., Norrish, M.: TacticToe: learning to prove with tactics. J. Autom. Reason. 65(2), 257\u2013286 (2021)","journal-title":"J. Autom. Reason."},{"key":"4_CR45","doi-asserted-by":"publisher","first-page":"109009","DOI":"10.1016\/j.ijar.2023.109009","volume":"162","author":"T Gauthier","year":"2023","unstructured":"Gauthier, T., Ols\u00e1k, M., Urban, J.: Alien coding. Int. J. Approx. Reason. 162, 109009 (2023)","journal-title":"Int. J. Approx. Reason."},{"issue":"1","key":"4_CR46","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"PC Gilmore","year":"1960","unstructured":"Gilmore, P.C.: A proof method for quantification theory: its justification and realization. IBM J. Res. Dev. 4(1), 28\u201335 (1960)","journal-title":"IBM J. Res. Dev."},{"key":"4_CR47","unstructured":"Glanois, C., et al.: Neuro-symbolic hierarchical rule induction. In: ICML 2022, pp. 7583\u20137615 (2022)"},{"key":"4_CR48","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-030-86205-3_10","volume-title":"Frontiers of Combining Systems","author":"ZA Goertzel","year":"2021","unstructured":"Goertzel, Z.A., Chvalovsk\u00fd, K., Jakub\u016fv, J., Ol\u0161\u00e1k, M., Urban, J.: Fast and slow enigmas and parental guidance. In: Konev, B., Reger, G. (eds.) Frontiers of Combining Systems. Lecture Notes in Computer Science(), vol. 12941, pp. 173\u2013191. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86205-3_10"},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Goertzel, Z.A.,\u00a0Jakub\u016fv, J.,\u00a0Urban, J.: ENIGMAWatch: ProofWatch meets ENIGMA. In: TABLEAUX 2019, volume 11714 of LNCS, pp. 374\u2013388 (2019)","DOI":"10.1007\/978-3-030-29026-9_21"},{"key":"4_CR50","unstructured":"Goller, C.: Learning search-control heuristics with folding architecture networks. In: ESANN 1999, pp. 45\u201350 (1999)"},{"key":"4_CR51","doi-asserted-by":"crossref","unstructured":"Goller, C., Kuchler, A.: Learning task-dependent distributed representations by backpropagation through structure. In: ICNN\u201996, pp. 347\u2013352. IEEE (1996)","DOI":"10.1109\/ICNN.1996.548916"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-319-21401-6_16","volume-title":"Automated Deduction - CADE-25","author":"T Gransden","year":"2015","unstructured":"Gransden, T., Walkinshaw, N., Raman, R.: SEPIA: search for proofs using inferred automata. In: Felty, A., Middeldorp, A. (eds.) Automated Deduction - CADE-25. Lecture Notes in Computer Science(), vol. 9195, pp. 246\u2013255. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_16"},{"key":"4_CR53","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-319-40229-1_22","volume-title":"Automated Reasoning","author":"K Hoder","year":"2016","unstructured":"Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning. Lecture Notes in Computer Science(), vol. 9706, pp. 313\u2013329. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_22"},{"key":"4_CR54","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction - CADE-23","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjorner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction - CADE-23. Lecture Notes in Computer Science(), vol. 6803, pp. 299\u2013314. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_23"},{"key":"4_CR55","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-030-81097-9_8","volume-title":"Intelligent Computer Mathematics","author":"EK Holden","year":"2021","unstructured":"Holden, E.K., Korovin, K.: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science(), vol. 12833, pp. 107\u2013123. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81097-9_8"},{"key":"4_CR56","unstructured":"Holden, E.K.:\u00a0Korovin, K.: Graph sequence learning for premise selection. CoRR, abs\/2303.15642 (2023)"},{"issue":"6","key":"4_CR57","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1561\/2200000081","volume":"14","author":"SB Holden","year":"2021","unstructured":"Holden, S.B.: Machine learning for automated theorem proving: Learning to solve SAT and QSAT. Found. Trends Mach. Learn. 14(6), 807\u2013989 (2021)","journal-title":"Found. Trends Mach. Learn."},{"key":"4_CR58","unstructured":"Huang, D., Dhariwal, P., Song, D., Sutskever, I.: GamePad: A learning environment for theorem proving. In: ICLR (2019)"},{"key":"4_CR59","unstructured":"Jakub\u016fv, J., et al.: MizAR 60 for Mizar 50. In: ITP 2023, volume 268 of LIPIcs, pp. 1\u201322 (2023)"},{"key":"4_CR60","series-title":"Lecture Notes in Computer Science()","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.) Automated Reasoning. Lecture Notes in Computer Science(), vol. 12167, pp. 448\u2013463. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_29"},{"key":"4_CR61","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-319-96418-8_29","volume-title":"Mathematical Software - ICMS 2018","author":"J Jakub\u016fv","year":"2018","unstructured":"Jakub\u016fv, J., Kaliszyk, C.: Unified ordering for superposition-based automated reasoning. In: Davenport, J., Kauers, M., Labahn, G., Urban, J. (eds.) Mathematical Software - ICMS 2018. Lecture Notes in Computer Science(), vol. 10931, pp. 245\u2013254. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96418-8_29"},{"key":"4_CR62","series-title":"Lecture Notes in Computer Science()","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.) Intelligent Computer Mathematics. Lecture Notes in Computer Science(), vol. 10383, pp. 292\u2013302. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_20"},{"key":"4_CR63","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-96812-4_11","volume-title":"Intelligent Computer Mathematics","author":"J Jakub\u016fv","year":"2018","unstructured":"Jakub\u016fv, J., Urban, J.: Enhancing ENIGMA given clause guidance. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science(), vol. 11006, pp. 118\u2013124. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_11"},{"issue":"3","key":"4_CR64","doi-asserted-by":"publisher","first-page":"237","DOI":"10.3233\/AIC-180761","volume":"31","author":"J Jakub\u016fv","year":"2018","unstructured":"Jakub\u016fv, J., Urban, J.: Hierarchical invention of theorem proving strategies. AI Commun. 31(3), 237\u2013250 (2018)","journal-title":"AI Commun."},{"key":"4_CR65","unstructured":"Jakub\u016fv, J.,\u00a0Urban, J.: Hammering Mizar by learning clause guidance (short paper). In: ITP 2019, volume 141 of LIPIcs, pp. 1\u20138 (2019)"},{"key":"4_CR66","unstructured":"Janota, M.,\u00a0Piepenbrock, J.,\u00a0Piotrowski, B.: Towards learning quantifier instantiation in SMT. In: Meel, K.S.,\u00a0Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pp. 1\u201318. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"4_CR67","unstructured":"Jiang, A.Q., et al.: Draft, sketch, and prove: guiding formal theorem provers with informal proofs. In: ICLR (2023)"},{"key":"4_CR68","unstructured":"Johansson, M., Smallbone, N.: Exploring mathematical conjecturing with large language models. In: NeSy, volume 3432 of CEUR Workshop Proceedings, pp. 62\u201377. CEUR-WS.org (2023)"},{"key":"4_CR69","unstructured":"Bayardo Jr, R.J., Schrag, R.: Using CSP look-back for real-world SAT instances. In: AAAI 97, pp. 203\u2013208. AAAI Press\/The MIT Press (1997)"},{"key":"4_CR70","doi-asserted-by":"publisher","first-page":"e20","DOI":"10.1017\/S0956796818000151","volume":"28","author":"R Jung","year":"2018","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018)","journal-title":"J. Funct. Program."},{"key":"4_CR71","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C.,\u00a0Urban, J.: Stronger automation for flyspeck: feature weighting and strategy evolution. In: PxTP 2013, volume\u00a014 of EPiC Series in Computing, pp. 87\u201395. EasyChair (2013)","DOI":"10.29007\/5gzr"},{"issue":"2","key":"4_CR72","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reason."},{"key":"4_CR73","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-662-48899-7_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: FEMaLeCoP: fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning. Lecture Notes in Computer Science(), vol. 9450, pp. 88\u201396. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_7"},{"key":"4_CR74","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jsc.2014.09.032","volume":"69","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69, 109\u2013128 (2015)","journal-title":"J. Symb. Comput."},{"issue":"3","key":"4_CR75","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reason. 55(3), 245\u2013256 (2015)","journal-title":"J. Autom. Reason."},{"key":"4_CR76","unstructured":"Kaliszyk, C., Urban, J., Michalewski, H., Ol\u0161\u00e1k, M.: Reinforcement learning of theorem proving. In: NeurIPS 2018, pp. 8836\u20138847 (2018)"},{"key":"4_CR77","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C.,\u00a0Urban, J.,\u00a0Vysko\u010dil, J.: Machine learner for automated reasoning 0.4 and 0.5. In: PAAR@IJCAR, volume\u00a031 of EPiC, pp. 60\u201366 (2014)","DOI":"10.29007\/shxj"},{"key":"4_CR78","unstructured":"Kaliszyk, C.,\u00a0Urban, J.,\u00a0Vysko\u010dil, J.: Efficient semantic features for automated reasoning over large theories. In: IJCAI 2015, pp. 3084\u20133090. AAAI Press (2015)"},{"key":"4_CR79","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-319-66107-0_2","volume-title":"Interactive Theorem Proving","author":"C Kaliszyk","year":"2017","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Automating formalization by statistical and semantic parsing of mathematics. In: Ayala-Rincon, M., Munoz, C.A. (eds.) Interactive Theorem Proving. Lecture Notes in Computer Science(), vol. 10499, pp. 12\u201327. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_2"},{"key":"4_CR80","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-319-08434-3_34","volume-title":"Intelligent Computer Mathematics","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J., Geuvers, H.: Developing corpus-based translation methods between informal and formal mathematics: project description. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science(), vol. 8543, pp. 435\u2013439. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_34"},{"key":"4_CR81","unstructured":"Ke, G., et al.: LightGBM: a highly efficient gradient boosting decision tree. In: NeurIPS 2017, pp. 3146\u20133154 (2017)"},{"key":"4_CR82","doi-asserted-by":"crossref","unstructured":"Komendantskaya, E.,\u00a0Heras, J.,\u00a0Grov, G.: Machine learning in proof general: interfacing interfaces. In: UITP, volume 118 of EPTCS, pp. 15\u201341 (2012)","DOI":"10.4204\/EPTCS.118.2"},{"key":"4_CR83","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning. Lecture Notes in Computer Science(), vol. 5195, pp. 292\u2013298. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24"},{"key":"4_CR84","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Inst-Gen - a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. Lecture Notes in Computer Science, vol. 7797, pp. 239\u2013270. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-37651-1_10"},{"key":"4_CR85","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.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 8044, pp. 1\u201335. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"4_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 7998, pp. 35\u201350. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_6"},{"issue":"2","key":"4_CR87","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."},{"key":"4_CR88","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O.,\u00a0Norrish, M.,\u00a0Owens, S.: CakeML: a verified implementation of ML. In: Principles of Programming Languages (POPL), pp. 179\u2013191. ACM Press (2014)","DOI":"10.1145\/2578855.2535841"},{"key":"4_CR89","unstructured":"Lample, G., et al.: Hypertree proof search for neural theorem proving. In: NeurIPS (2022)"},{"key":"4_CR90","unstructured":"Landwehr, N.,\u00a0Kersting, K., Raedt, L.D.: nFOIL: integrating na\u00efve Bayes and FOIL. In: AAAI 2005, pp. 795\u2013800. AAAI Press\/The MIT Press (2005)"},{"key":"4_CR91","unstructured":"Landwehr, N.,\u00a0Passerini, A., Raedt, L.D.,\u00a0Frasconi, P.: kFOIL: learning simple relational kernels. In: AAAI 2006, pp. 389\u2013394. AAAI Press (2006)"},{"key":"4_CR92","unstructured":"Langley, P.: BACON: a production system that discovers empirical laws. In: International Joint Conference on Artificial Intelligence (1977)"},{"key":"4_CR93","unstructured":"Lenat, D.: An artificial intelligence approach to discovery in mathematics. PhD thesis, Stanford University, Stanford, USA (1976)"},{"key":"4_CR94","doi-asserted-by":"crossref","unstructured":"Loos, S.M.,\u00a0Irving, G.,\u00a0Szegedy, C.,\u00a0Kaliszyk, C.: Deep network guided proof search. In: LPAR-21, volume\u00a046 of EPiC Series in Computing, pp. 85\u2013105. EasyChair (2017)","DOI":"10.29007\/8mwc"},{"key":"4_CR95","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/978-3-319-94205-6_43","volume-title":"Automated Reasoning","author":"JC L\u00f3pez-Hern\u00e1ndez","year":"2018","unstructured":"L\u00f3pez-Hern\u00e1ndez, J.C., Korovin, K.: An abstraction-refinement framework for reasoning with large theories. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning. Lecture Notes in Computer Science(), vol. 10900, pp. 663\u2013679. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_43"},{"key":"4_CR96","unstructured":"Manhaeve, R., Dumancic, S., Kimmig, A., Demeester, T., Raedt, L.D.: DeepProbLog: neural probabilistic logic programming. In: NeurIPS 2018, pp. 3753\u20133763 (2018)"},{"key":"4_CR97","doi-asserted-by":"publisher","first-page":"103504","DOI":"10.1016\/j.artint.2021.103504","volume":"298","author":"R Manhaeve","year":"2021","unstructured":"Manhaeve, R., Dumancic, S., Kimmig, A., Demeester, T., Raedt, L.D.: Neural probabilistic logic programming in DeepProbLog. Artif. Intell. 298, 103504 (2021)","journal-title":"Artif. Intell."},{"key":"4_CR98","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.) 10th International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 449, pp. 663\u2013664. Springer, Berlin (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_131"},{"key":"4_CR99","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-25984-8_28","volume-title":"Automated Reasoning","author":"J Meng","year":"2004","unstructured":"Meng, J., Paulson, L.C.: Experiments on supporting interactive proof using resolution. In: Basin, D., Rusinowitch, M. (eds.) Automated Reasoning. Lecture Notes in Computer Science(), vol. 3097, pp. 372\u2013384. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_28"},{"issue":"1","key":"4_CR100","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logic 7(1), 41\u201357 (2009)","journal-title":"J. Appl. Logic"},{"key":"4_CR101","unstructured":"Mikolov, T.,\u00a0Chen, K.,\u00a0Corrado, G.,\u00a0Dean, J.: Efficient estimation of word representations in vector space. arXiv preprint: arXiv:1301.3781 (2013)"},{"key":"4_CR102","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F.,\u00a0Zhao, Y.,\u00a0Zhang, L.,\u00a0Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC 2001, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"4_CR103","doi-asserted-by":"crossref","unstructured":"Nagashima, Y.,\u00a0He, Y.: PaMpeR: proof method recommendation system for Isabelle\/HOL. In:\u00a0Huchard, M.,\u00a0K\u00e4stner, C.,\u00a0Fraser, G. (eds.) Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018, pp. 362\u2013372. ACM (2018)","DOI":"10.1145\/3238147.3238210"},{"issue":"3","key":"4_CR104","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/TIT.1956.1056797","volume":"2","author":"A Newell","year":"1956","unstructured":"Newell, A., Simon, H.: The logic theory machine-a complex information processing system. IRE Trans. Inf. Theory 2(3), 61\u201379 (1956)","journal-title":"IRE Trans. Inf. Theory"},{"key":"4_CR105","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R.,\u00a0Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning (in 2 volumes), pp. 371\u2013443 (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"4_CR106","unstructured":"Ol\u0161\u00e1k, M.,\u00a0Kaliszyk, C.,\u00a0Urban, J.: Property invariant embedding for automated reasoning. In: ECAI 2020, volume 325, pp. 1395\u20131402. IOS Press (2020)"},{"issue":"1\u20132","key":"4_CR107","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":"4_CR108","doi-asserted-by":"publisher","unstructured":"Otten, J.,\u00a0Bibel, W.: Advances in connection-based automated theorem proving. In: Hinchey, M., Bowen, J., Olderog, E.R. (eds.) Provably Correct Systems. NASA Monographs in Systems and Software Engineering, pp. 211\u2013241. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-48628-4_9","DOI":"10.1007\/978-3-319-48628-4_9"},{"key":"4_CR109","unstructured":"Piepenbrock, J.,\u00a0Janota, M.,\u00a0Urban, J.,\u00a0Jakub\u016fv, J.: First experiments with neural cvc5 (2024). http:\/\/grid01.ciirc.cvut.cz\/~mptp\/cvc5-gnn.pdf"},{"key":"4_CR110","unstructured":"Piepenbrock, J.,\u00a0Urban, J.,\u00a0Korovin, K.,\u00a0Ol\u0161\u00e1k, M.,\u00a0Heskes, T.,\u00a0Janota, M.: Machine learning meets the Herbrand universe. CoRR, abs\/2210.03590 (2022)"},{"key":"4_CR111","series-title":"pp","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-030-80223-3_31","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2021","author":"N Pimpalkhare","year":"2021","unstructured":"Pimpalkhare, N., Mora, F., Polgreen, E., Seshia, S.A.: MedleySolver: online SMT algorithm selection. In: Li, C.-M., Many\u00e0, F. (eds.) Theory and Applications of Satisfiability Testing - SAT 2021. pp, pp. 453\u2013470. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_31"},{"key":"4_CR112","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-031-43513-3_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"B Piotrowski","year":"2023","unstructured":"Piotrowski, B., Mir, R.F., Ayers, E.: Machine-Learned Premise Selection for Lean. In: Ramanayake, R., Urban, J. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science(), vol. 14278, pp. 175\u2013186. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43513-3_10"},{"key":"4_CR113","doi-asserted-by":"publisher","unstructured":"BPiotrowski, B., Urban, J.: ATPboost: learning premise selection in binary setting with ATP feedback. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning. Lecture Notes in Computer Science(), vol. 10900, pp. 566\u2013574. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_37","DOI":"10.1007\/978-3-319-94205-6_37"},{"key":"4_CR114","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-030-53518-6_23","volume-title":"Intelligent Computer Mathematics","author":"B Piotrowski","year":"2020","unstructured":"Piotrowski, B., Urban, J.: Guiding inferences in connection tableau by recurrent neural networks. In: Benzmuller, C., Miller, B. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science(), vol. 12236, pp. 309\u2013314. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_23"},{"key":"4_CR115","unstructured":"Piotrowski, B., Urban, J.: Stateful premise selection by recurrent neural networks. In: LPAR 2020, volume\u00a073 of EPiC, pp. 409\u2013422. EasyChair (2020)"},{"key":"4_CR116","unstructured":"Purgal, S.J., Cerna, D.M.,\u00a0Kaliszyk, C.: Differentiable inductive logic programming in high-dimensional space. CoRR, abs\/2208.06652 (2022)"},{"key":"4_CR117","doi-asserted-by":"crossref","unstructured":"Purgal, S.J.,\u00a0Kaliszyk, C.: Adversarial learning to reason in an arbitrary logic. In: FLAIRS 2022 (2022)","DOI":"10.32473\/flairs.v35i.130648"},{"issue":"8","key":"4_CR118","doi-asserted-by":"publisher","first-page":"2057","DOI":"10.1093\/logcom\/exab006","volume":"31","author":"SJ Purgal","year":"2021","unstructured":"Purgal, S.J., Parsert, J., Kaliszyk, C.: A study of continuous vector representations for theorem proving. J. Log. Comput. 31(8), 2057\u20132083 (2021)","journal-title":"J. Log. Comput."},{"key":"4_CR119","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BF00117105","volume":"5","author":"JR Quinlan","year":"1990","unstructured":"Quinlan, J.R.: Learning logical definitions from relations. Mach. Learn. 5, 239\u2013266 (1990)","journal-title":"Mach. Learn."},{"key":"4_CR120","unstructured":"Rabe, M.N.,\u00a0Lee, D.,\u00a0Bansal, K.,\u00a0Szegedy, C.: Mathematical reasoning via self-supervised skip-tree training. In: ICLR. OpenReview.net (2021)"},{"key":"4_CR121","doi-asserted-by":"crossref","unstructured":"Ramakrishnan, I.V.,\u00a0Sekar, R.,\u00a0Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning (in 2 volumes), pp. 1853\u20131964 (2001)","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"4_CR122","unstructured":"Rawson, M.,\u00a0Reger, G.: Directed graph networks for logical reasoning (extended abstract). In: PAAR 2020, volume 2752 of CEUR Workshop Proceedings, pp. 109\u2013119. CEUR-WS.org (2020)"},{"key":"4_CR123","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-030-86059-2_11","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Rawson","year":"2021","unstructured":"Rawson, M., Reger, G.: lazyCoP: Lazy paramodulation meets neurally guided search. In: Das, A., Negri, S. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science(), vol. 12842, pp. 187\u2013199. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_11"},{"key":"4_CR124","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-319-21401-6_28","volume-title":"Automated Deduction - CADE-25","author":"G Reger","year":"2015","unstructured":"Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A., Middeldorp, A. (eds.) Automated Deduction - CADE-25. Lecture Notes in Computer Science(), vol. 9195, pp. 399\u2013415. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_28"},{"issue":"1","key":"4_CR125","doi-asserted-by":"publisher","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 (JACM) 12(1), 23\u201341 (1965)","journal-title":"J. ACM (JACM)"},{"key":"4_CR126","unstructured":"Robinson, J.A.,\u00a0Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)"},{"key":"4_CR127","unstructured":"Rockt\u00e4schel, T., Riedel, S.: End-to-end differentiable proving. In: NeurIPS 2017, pp. 3788\u20133800 (2017)"},{"key":"4_CR128","unstructured":"Rute, J.,\u00a0Ols\u00e1k, M.,\u00a0Blaauwbroek, L., Massolo, F.I.S.,\u00a0Piepenbrock, J.,\u00a0Pestun, V.: Graph2Tac: learning hierarchical representations of math concepts in theorem proving. CoRR, abs\/2401.02949 (2024)"},{"key":"4_CR129","doi-asserted-by":"crossref","unstructured":"Sanchez-Stern, A.,\u00a0Alhessi, Y., Saul, L.K.,\u00a0Lerner, S.: Generating correctness proofs with neural networks. CoRR, abs\/1907.07794 (2019)","DOI":"10.1145\/3394450.3397466"},{"issue":"2","key":"4_CR130","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3593374","volume":"45","author":"A Sanchez-Stern","year":"2023","unstructured":"Sanchez-Stern, A., First, E., Zhou, T., Kaufman, Z., Brun, Y., Ringer, T.: Passport: improving automated formal verification using identifiers. ACM Trans. Program. Lang. Syst. 45(2), 1\u201330 (2023)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"4_CR131","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/TNN.2008.2005605","volume":"20","author":"F Scarselli","year":"2009","unstructured":"Scarselli, F., Gori, M., Tsoi, A.C., Hagenbuchner, M., Monfardini, G.: The graph neural network model. IEEE Trans. Neural Netw. 20(1), 61\u201380 (2009)","journal-title":"IEEE Trans. Neural Netw."},{"key":"4_CR132","unstructured":"Schaeffer, R., Miranda, B., Koyejo, S.: Are emergent abilities of large language models a mirage? In:\u00a0Oh, A.,\u00a0Neumann, T.,\u00a0Globerson, A.,\u00a0Saenko, K.,\u00a0Hardt, M.,\u00a0Levine, S. (eds.) Advances in Neural Information Processing Systems, vol.\u00a036, pp. 55565\u201355581. Curran Associates, Inc. (2023)"},{"key":"4_CR133","unstructured":"Sch\u00e4fer, S.,\u00a0Schulz, S.: Breeding theorem proving heuristics with genetic algorithms. In: GCAI, volume\u00a036 of EPiC, pp. 263\u2013274 (2015)"},{"key":"4_CR134","unstructured":"Schulz, S.: Explanation based learning for distributed equational deduction. Diplomarbeit in Informatik, Fachbereich Informatik, Univ. Kaiserslautern (1995)"},{"key":"4_CR135","unstructured":"Schulz, S.: Learning Search Control Knowledge for Equational Deduction, volume 230 of DISKI. Infix Akademische Verlagsgesellschaft (2000)"},{"key":"4_CR136","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/3-540-45422-5_23","volume-title":"KI 2001: Advances in Artificial Intelligence","author":"S Schulz","year":"2001","unstructured":"Schulz, S.: Learning search control knowledge for equational theorem proving. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI 2001: Advances in Artificial Intelligence. Lecture Notes in Computer Science(), vol. 2174, pp. 320\u2013334. Springer, Berlin (2001). https:\/\/doi.org\/10.1007\/3-540-45422-5_23"},{"issue":"2\u20133","key":"4_CR137","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":"4_CR138","doi-asserted-by":"publisher","unstructured":"chulz, S., Cruanes, S., Vukmirovic, P.: Faster, Higher, Stronger: E 2.3. In: Fontaine, P. (eds.) Automated Deduction \u2013 CADE 27. Lecture Notes in Computer Science(), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"4_CR139","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-319-40229-1_23","volume-title":"Automated Reasoning","author":"S Schulz","year":"2016","unstructured":"Schulz, S., M\u00f6hrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning. Lecture Notes in Computer Science(), vol. 9706, pp. 330\u2013345. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_23"},{"key":"4_CR140","series-title":"pp","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-030-72013-1_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Scott","year":"2021","unstructured":"Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V.: MachSMT: a machine learning-based algorithm selector for SMT solvers. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp, pp. 303\u2013325. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_16"},{"key":"4_CR141","unstructured":"Selsam, D.,\u00a0Lamm, M.,\u00a0B\u00fcnz, B.,\u00a0Liang, P.,\u00a0de\u00a0Moura, L., Dill, D.L.: Learning a SAT solver from single-bit supervision. In: ICLR 2019. OpenReview.net (2019)"},{"key":"4_CR142","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809682","volume-title":"Kernel Methods for Pattern Analysis","author":"J Shawe-Taylor","year":"2004","unstructured":"Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, New York (2004)"},{"key":"4_CR143","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: ICCAD 1996, pp. 220\u2013227. IEEE Computer Society\/ACM (1996)"},{"key":"4_CR144","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-79876-5_31","volume-title":"Automated Deduction - CADE 28","author":"M Suda","year":"2021","unstructured":"Suda, M.: Improving ENIGMA-style clause selection while learning from history. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28. Lecture Notes in Computer Science(), vol. 12699, pp. 543\u2013561. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_31"},{"key":"4_CR145","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-030-86205-3_11","volume-title":"Frontiers of Combining Systems","author":"M Suda","year":"2021","unstructured":"Suda, M.: Vampire with a brain is a good ITP hammer. In: Konev, B., Reger, G. (eds.) Frontiers of Combining Systems. Lecture Notes in Computer Science(), vol. 12941, pp. 192\u2013209. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86205-3_11"},{"key":"4_CR146","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning - An Introduction. Adaptive Computation and Machine Learning. MIT Press, Cambridge (1998)"},{"key":"4_CR147","unstructured":"Topan, S.,\u00a0Rolnick, D.,\u00a0Si, X.: Techniques for symbol grounding with SATNet. In: NeurIPS 2021, vol.\u00a034, pp. 20733\u201320744. Curran Associates, Inc. (2021)"},{"key":"4_CR148","unstructured":"Urban, J.: Experimenting with machine learning in automatic theorem proving. Master\u2019s thesis, Charles University, Prague (1998). English summary at https:\/\/www.ciirc.cvut.cz\/~urbanjo3\/MScThesisPaper.pdf"},{"key":"4_CR149","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-36469-2_16","volume-title":"Mathematical Knowledge Management","author":"J Urban","year":"2003","unstructured":"Urban, J.: Translating Mizar for first order theorem provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) Mathematical Knowledge Management. Lecture Notes in Computer Science, vol. 2594, pp. 203\u2013215. Springer, Berlin (2003). https:\/\/doi.org\/10.1007\/3-540-36469-2_16"},{"issue":"3\u20134","key":"4_CR150","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s10817-004-6245-1","volume":"33","author":"J Urban","year":"2004","unstructured":"Urban, J.: MPTP - motivation, implementation, first experiments. J. Autom. Reasoning 33(3\u20134), 319\u2013339 (2004)","journal-title":"J. Autom. Reasoning"},{"issue":"1\u20132","key":"4_CR151","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":"4_CR152","unstructured":"Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: ESARLT, volume 257 of CEUR. CEUR-WS.org (2007)"},{"key":"4_CR153","doi-asserted-by":"crossref","unstructured":"Urban, J.: BliStr: the blind Strategymaker. In: GCAI 2015, volume\u00a036 of EPiC, pp. 312\u2013319 (2015)","DOI":"10.29007\/8n7m"},{"key":"4_CR154","unstructured":"Urban, J.: No one shall drive us from the semantic AI paradise of computer-understandable math and science! https:\/\/slideslive.com\/38909911\/no-one-shall-drive-us-from-the-semantic-ai-paradise-of-computerunderstandable-math-and-science (2018). Keynote at the Artificial General Intelligence Conference (AGI\u201918)"},{"key":"4_CR155","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-030-53518-6_24","volume-title":"Intelligent Computer Mathematics","author":"J Urban","year":"2020","unstructured":"Urban, J., Jakub\u016fv, J.: First neural conjecturing datasets and experiments. In: Benzmuller, C., Miller, B. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science(), vol. 12236, pp. 315\u2013323. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_24"},{"key":"4_CR156","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning. Lecture Notes in Computer Science(), vol. 5195, pp. 441\u2013456. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_37"},{"key":"4_CR157","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-22119-4_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Urban","year":"2011","unstructured":"Urban, J., Vysko\u010dil, J., \u0160tep\u00e1nek, P.: MaLeCoP machine learning connection prover. In: Brunnler, K., Metcalfe, G. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science(), vol. 6793, pp. 263\u2013277. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22119-4_21"},{"issue":"3","key":"4_CR158","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. Reasoning 16(3), 223\u2013239 (1996)","journal-title":"J. Autom. Reasoning"},{"key":"4_CR159","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 8559, pp. 696\u2013710. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46"},{"key":"4_CR160","unstructured":"Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: NIPS\u201917, pp. 2783-2793, Red Hook, NY, USA. Curran Associates Inc. (2017)"},{"key":"4_CR161","unstructured":"Wang, P., Donti, P.L.,\u00a0Wilder, B., Kolter, J.Z.: SATNet: bridging deep learning and logical reasoning with a differentiable satisfiability solver. In: ICML 2019, volume\u00a097, pp. 6545\u20136554. PMLR (2019)"},{"key":"4_CR162","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-96812-4_22","volume-title":"Intelligent Computer Mathematics","author":"Q Wang","year":"2018","unstructured":"Wang, Q., Kaliszyk, C., Urban, J.: First experiments with neural translation of informal to formal mathematics. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science(), vol. 11006, pp. 255\u2013270. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_22"},{"key":"4_CR163","unstructured":"Yang, K., Deng, J.: Learning to prove theorems via interacting with proof assistants. In: ICML-36, volume\u00a097 of PMLR, pp. 6984\u20136994 (2019)"},{"key":"4_CR164","unstructured":"Yang, K., et al.: LeanDojo: theorem proving with retrieval-augmented language models. arXiv preprint: arXiv:2306.15626 (2023)"},{"key":"4_CR165","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-031-43369-6_13","volume-title":"Frontiers of Combining Systems","author":"L Zhang","year":"2023","unstructured":"Zhang, L., Blaauwbroek, L., Kaliszyk, C., Urban, J.: Learning proof transformations and its applications in interactive theorem proving. In: Sattler, U., Suda, M. (eds.) Frontiers of Combining Systems. Lecture Notes in Computer Science(), vol. 14279, pp. 236\u2013254. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43369-6_13"},{"key":"4_CR166","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-030-86059-2_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"Z Zombori","year":"2021","unstructured":"Zombori, Z., Csisz\u00e1rik, A., Michalewski, H., Kaliszyk, C., Urban, J.: Towards finding longer proofs. In: Das, A., Negri, S. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science(), vol. 12842, pp. 167\u2013186. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_10"},{"key":"4_CR167","series-title":"Lecture Notes in Computer Science()","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-030-86059-2_13","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"Z Zombori","year":"2021","unstructured":"Zombori, Z., Urban, J., Ol\u0161\u00e1k, M.: The role of entropy in guiding a connection prover. In: Das, A., Negri, S. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science(), vol. 12842, pp. 218\u2013235. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_13"}],"container-title":["Lecture Notes in Computer Science","Logics and Type Systems in Theory and Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-61716-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,20]],"date-time":"2024-11-20T15:23:55Z","timestamp":1732116235000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-61716-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031617157","9783031617164"],"references-count":167,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-61716-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"22 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}