{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:35:42Z","timestamp":1762324542673,"version":"3.37.3"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030290061"},{"type":"electronic","value":"9783030290078"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29007-8_3","type":"book-chapter","created":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T19:10:06Z","timestamp":1566414606000},"page":"40-56","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Neurally-Guided, Parallel Theorem Prover"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"first","affiliation":[]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,14]]},"reference":[{"key":"3_CR1","volume-title":"The Lambda Calculus","author":"HP Barendregt","year":"1984","unstructured":"Barendregt, H.P., et al.: The Lambda Calculus. North-Holland, Amsterdam (1984)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Bowman, S.R., Potts, C., Manning, C.D.: Recursive neural networks can learn logical semantics. arXiv preprint \n                      arXiv:1406.1827\n                      \n                     (2014)","DOI":"10.18653\/v1\/W15-4002"},{"issue":"2","key":"3_CR3","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s10817-014-9301-5","volume":"53","author":"JP Bridge","year":"2014","unstructured":"Bridge, J.P., Holden, S.B., Paulson, L.C.: Machine learning for first-order theorem proving. J. Autom. Reason. 53(2), 141\u2013172 (2014)","journal-title":"J. Autom. Reason."},{"key":"3_CR4","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":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"3_CR5","unstructured":"Defferrard, M., Bresson, X., Vandergheynst, P.: Convolutional neural networks on graphs with fast localized spectral filtering. In: Advances in Neural Information Processing Systems, pp. 3844\u20133852 (2016)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Deters, M., Reynolds, A., King, T., Barrett, C.W., Tinelli, C.: A tour of CVC4: how it works, and how to use it. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 October 2014, p. 7 (2014)","DOI":"10.1109\/FMCAD.2014.6987586"},{"key":"3_CR7","unstructured":"Evans, R., Saxton, D., Amos, D., Kohli, P., Grefenstette, E.: Can neural networks understand logical entailment? arXiv preprint \n                      arXiv:1802.08535\n                      \n                     (2018)"},{"key":"3_CR8","unstructured":"F\u00e4rber, M., Kaliszyk, C., Urban, J.: Monte Carlo connection prover. arXiv preprint \n                      arXiv:1611.05990\n                      \n                     (2016)"},{"key":"3_CR9","unstructured":"Fey, M., Lenssen, J.E.: Fast graph representation learning with PyTorch geometric. In: ICLR Workshop on Representation Learning on Graphs and Manifolds (2019)"},{"key":"3_CR10","unstructured":"Gao, H., Ji, S.: Graph U-Net (2018). Preprint: \n                      https:\/\/openreview.net\/forum?id=HJePRoAct7"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"issue":"2","key":"3_CR12","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reason. 3(2), 153\u2013245 (2010)","journal-title":"J. Formalized Reason."},{"key":"3_CR13","volume-title":"Neural Networks: A Comprehensive Foundation","author":"S Haykin","year":"1994","unstructured":"Haykin, S.: Neural Networks: A Comprehensive Foundation. Prentice Hall PTR, Upper Saddle River (1994)"},{"key":"3_CR14","unstructured":"Irving, G., Szegedy, C., Alemi, A.A., Een, N., Chollet, F., Urban, J.: DeepMath \u2013 deep sequence models for premise selection. In: Advances in Neural Information Processing Systems, pp. 2235\u20132243 (2016)"},{"key":"3_CR15","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-62075-6_20"},{"key":"3_CR16","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.) LPAR 2015. LNCS, vol. 9450, pp. 88\u201396. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-48899-7_7"},{"key":"3_CR17","unstructured":"Kaliszyk, C., Urban, J., Michalewski, H., Ol\u0161\u00e1k, M.: Reinforcement learning of theorem proving. In: Advances in Neural Information Processing Systems, pp. 8822\u20138833 (2018)"},{"key":"3_CR18","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-36675-8_8"},{"key":"3_CR19","unstructured":"Kipf, T.N., Welling, M.: Semi-supervised classification with graph convolutional networks. arXiv preprint \n                      arXiv:1609.02907\n                      \n                     (2016)"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-319-62075-6_21","volume-title":"Intelligent Computer Mathematics","author":"E Komendantskaya","year":"2017","unstructured":"Komendantskaya, E., Heras, J.: Proof mining with dependent types. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 303\u2013318. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-62075-6_21"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24"},{"key":"3_CR22","unstructured":"Krizhevsky, A., Sutskever, I., Hinton, G.E.: ImageNet classification with deep convolutional neural networks. In: Advances in Neural Information Processing Systems, pp. 1097\u20131105 (2012)"},{"key":"3_CR23","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.) ITP 2013. LNCS, vol. 7998, pp. 35\u201350. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39634-2_6"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-38574-2_28","volume-title":"Automated Deduction \u2013 CADE-24","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Schulz, S., Urban, J.: E-MaLeS 1.1. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 407\u2013413. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-38574-2_28"},{"issue":"2","key":"3_CR25","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":"3_CR26","unstructured":"Loos, S., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. arXiv preprint \n                      arXiv:1701.06972\n                      \n                     (2017)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-642-22119-4_18","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Otten","year":"2011","unstructured":"Otten, J.: A non-clausal connection calculus. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 226\u2013241. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22119-4_18"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-319-40229-1_21","volume-title":"Automated Reasoning","author":"J Otten","year":"2016","unstructured":"Otten, J.: nanoCoP: A non-clausal connection prover. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 302\u2013312. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40229-1_21"},{"key":"3_CR29","unstructured":"Paszke, A., et al.: Automatic differentiation in PyTorch (2017)"},{"key":"3_CR30","unstructured":"Rawson, M., Reger, G.: Dynamic strategy priority: empower the strong and abandon the weak. In: AITP 2018 (2018)"},{"key":"3_CR31","unstructured":"Rawson, M., Reger, G.: Towards an efficient architecture for intelligent theorem provers. In: AITP 2019 (2019)"},{"key":"3_CR32","unstructured":"Reger, G., Suda, M., Voronkov, A.: The challenges of evaluating a new feature in Vampire. In: Vampire Workshop, pp. 70\u201374 (2014)"},{"issue":"2, 3","key":"3_CR33","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."},{"issue":"1\u20132","key":"3_CR34","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","volume":"36","author":"A Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. J. Symb. Comput. 36(1\u20132), 101\u2013115 (2003)","journal-title":"J. Symb. Comput."},{"key":"3_CR35","volume-title":"Handbook of Automated Reasoning","author":"AJ Robinson","year":"2001","unstructured":"Robinson, A.J., Voronkov, A.: Handbook of Automated Reasoning, vol. 1. Gulf Professional Publishing, Houston (2001)"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-319-93417-4_38","volume-title":"The Semantic Web","author":"M Schlichtkrull","year":"2018","unstructured":"Schlichtkrull, M., Kipf, T.N., Bloem, P., van\u00a0den Berg, R., Titov, I., Welling, M.: Modeling relational data with graph convolutional networks. In: Gangemi, A., et al. (eds.) ESWC 2018. LNCS, vol. 10843, pp. 593\u2013607. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-93417-4_38"},{"issue":"2, 3","key":"3_CR37","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - A brainiac theorem prover. AI Commun. 15(2, 3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"issue":"1","key":"3_CR38","first-page":"1929","volume":"15","author":"N Srivastava","year":"2014","unstructured":"Srivastava, N., Hinton, G., Krizhevsky, A., Sutskever, I., Salakhutdinov, R.: Dropout: a simple way to prevent neural networks from overfitting. J. Mach. Learn. Res. 15(1), 1929\u20131958 (2014)","journal-title":"J. Mach. Learn. Res."},{"issue":"04","key":"3_CR39","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1142\/S0218001409007326","volume":"23","author":"Y Sun","year":"2009","unstructured":"Sun, Y., Wong, A.K., Kamel, M.S.: Classification of imbalanced data: a review. Int. J. Pattern Recogn. Artif. Intell. 23(04), 687\u2013719 (2009)","journal-title":"Int. J. Pattern Recogn. Artif. Intell."},{"key":"3_CR40","unstructured":"Sutcliffe, G., Melville, S.: The practice of clausification in automatic theorem proving (1996)"},{"key":"3_CR41","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/B978-0-444-81704-4.50015-6","volume":"14","author":"CB Suttner","year":"1994","unstructured":"Suttner, C.B., Schumann, J.: Parallel automated theorem proving. Mach. Intell. Pattern Recogn. 14, 209\u2013257 (1994). Elsevier","journal-title":"Mach. Intell. Pattern Recogn."},{"issue":"1\u20132","key":"3_CR42","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1\u20132), 21\u201343 (2006)","journal-title":"J. Autom. Reason."},{"key":"3_CR43","unstructured":"Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: ESARLT, vol. 257 (2007)"},{"key":"3_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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., \u0160t\u011bp\u00e1nek, P.: MaLeCoP machine learning connection prover. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 263\u2013277. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22119-4_21"},{"key":"3_CR45","unstructured":"Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: Advances in Neural Information Processing Systems, pp. 2786\u20132796 (2017)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29007-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T19:12:14Z","timestamp":1566414734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-29007-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030290061","9783030290078"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29007-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","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":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.frocos2019.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":"30","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":"20","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":"67% - 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":"3.1","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":"3","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)"}}]}}