{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T02:47:06Z","timestamp":1779331626394,"version":"3.51.4"},"reference-count":76,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Pattern Anal. Mach. Intell."],"published-print":{"date-parts":[[2023,1,1]]},"DOI":"10.1109\/tpami.2022.3140382","type":"journal-article","created":{"date-parts":[[2022,1,4]],"date-time":"2022-01-04T20:33:23Z","timestamp":1641328403000},"page":"738-751","source":"Crossref","is-referenced-by-count":8,"title":["Learning to Guide a Saturation-Based Theorem Prover"],"prefix":"10.1109","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1449-5115","authenticated-orcid":false,"given":"Ibrahim","family":"Abdelaziz","sequence":"first","affiliation":[{"name":"IBM Research, Armonk, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7327-7508","authenticated-orcid":false,"given":"Maxwell","family":"Crouse","sequence":"additional","affiliation":[{"name":"IBM Research, Armonk, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bassem","family":"Makni","sequence":"additional","affiliation":[{"name":"Arizona State University, Tempe, AZ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vernon","family":"Austel","sequence":"additional","affiliation":[{"name":"IBM Research, Armonk, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristina","family":"Cornelio","sequence":"additional","affiliation":[{"name":"Samsung AI, Cambridge, U.K."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shajith","family":"Ikbal","sequence":"additional","affiliation":[{"name":"IBM Research, Armonk, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavan","family":"Kapanipathi","sequence":"additional","affiliation":[{"name":"IBM Research, Armonk, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4147-3328","authenticated-orcid":false,"given":"Ndivhuwo","family":"Makondo","sequence":"additional","affiliation":[{"name":"IBM Research, Armonk, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kavitha","family":"Srinivas","sequence":"additional","affiliation":[{"name":"IBM Research, Armonk, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Witbrock","sequence":"additional","affiliation":[{"name":"University of Auckland, Auckland, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1137-1344","authenticated-orcid":false,"given":"Achille","family":"Fokoue","sequence":"additional","affiliation":[{"name":"IBM Research, Armonk, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref73","article-title":"Automated theorem proving, fast and slow","author":"rawson","year":"2021","journal-title":"EasyChair Preprint"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29007-8_3"},{"key":"ref71","first-page":"1395","article-title":"Property invariant embedding for automated reasoning","author":"ol\u0161\u00e1k","year":"2020","journal-title":"Proc 24th Eur Conf Artif Intell"},{"key":"ref70","article-title":"Learning representations of logical formulae using graph neural networks","author":"glorot","year":"2019"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_8"},{"key":"ref74","article-title":"Learning a SAT solver from single-bit supervision","author":"selsam","year":"2019"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D18-1433"},{"key":"ref75","article-title":"The logical expressiveness of graph neural networks","author":"barcel\u00f3","year":"2019","journal-title":"Proc Int Conf Learn Representations"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2016.496"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D15-1166"},{"key":"ref32","first-page":"353","article-title":"Equational reasoning in saturation-based theorem proving","volume":"1","author":"bachmair","year":"1998","journal-title":"Automated Deduction—A Basis for Appl"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"ref30","author":"enderton","year":"2001","journal-title":"A Mathematical Introduction to Logic"},{"key":"ref37","first-page":"5998","article-title":"Attention is all you need","author":"vaswani","year":"2017","journal-title":"Proc Int Conf Neural Inf Process"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2016.90"},{"key":"ref35","first-page":"5981","article-title":"R3: Reinforced ranker-reader for open-domain question answering","author":"wang","year":"2018","journal-title":"Proc AAAI Conf Artif Intell"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/TNN.1998.712192"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"ref62","first-page":"109","article-title":"Directed graph networks for logical reasoning","author":"rawson","year":"2020","journal-title":"Proc Workshop Practical Aspects Automated Reasoning"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_13"},{"key":"ref63","first-page":"409","article-title":"Stateful premise selection by recurrent neural networks","author":"piotrowski","year":"2020","journal-title":"Proc 23rd Int Conf Log Program Artif Intell Reasoning"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9440-6"},{"key":"ref27","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","article-title":"MPTP 0.2: Design, implementation, and initial experiments","volume":"37","author":"urban","year":"2006","journal-title":"J Automated Reasoning"},{"key":"ref65","first-page":"146","article-title":"Guiding inference with policy search reinforcement learning","author":"taylor","year":"2007","journal-title":"Proc 20th Int Florida Artif Intell Res Soc Conf"},{"key":"ref66","article-title":"A survey of reinforcement learning in relational domains","author":"van otterlo","year":"2005"},{"key":"ref29","author":"bergmann","year":"2013","journal-title":"The Logic Book"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1007\/BF01190829"},{"key":"ref68","article-title":"HOList: An environment for machine learning of higher-order theorem proving (extended version)","author":"bansal","year":"2019","journal-title":"CoRR"},{"key":"ref69","article-title":"Learning to prove from synthetic theorems","author":"ayg\u00fcn","year":"2020"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/HOL.1991.596292"},{"key":"ref20","article-title":"Learning to reason in large theories without imitation","author":"bansal","year":"2019","journal-title":"CoRR"},{"key":"ref22","article-title":"Learning heuristics for automated reasoning through deep reinforcement learning","author":"lederman","year":"2018","journal-title":"CoRR"},{"key":"ref21","article-title":"Automated theorem proving in intuitionistic propositional logic by deep reinforcement learning","author":"kusumoto","year":"2018","journal-title":"CoRR"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"ref23","article-title":"Learning to progressively plan","author":"chen","year":"2018","journal-title":"CoRR"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9330-8"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v35i7.16780"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9286-5"},{"key":"ref51","first-page":"153","article-title":"Mizar in a nutshell","volume":"3","author":"grabowski","year":"2010","journal-title":"Journal of Formalized Reasoning"},{"key":"ref59","first-page":"2783","article-title":"Premise selection for theorem proving by deep graph embedding","author":"wang","year":"2017","journal-title":"Proc Int Conf Neural Inf Process"},{"key":"ref58","first-page":"2243","article-title":"DeepMath - Deep sequence models for premise selection","author":"alemi","year":"2016","journal-title":"Proc 30th Int Conf Neural Inf Process Syst"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9362-8"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9286-5"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(03)00037-3"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693176"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_25"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9407-7"},{"key":"ref10","first-page":"85","article-title":"Deep network guided proof search","author":"loos","year":"2017","journal-title":"Proc 21st Int Conf Log Program Artif Intell Reasoning"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_12"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1126\/science.aar6404"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i03.5689"},{"key":"ref13","article-title":"Hammering Mizar by learning clause guidance","author":"jakubuv","year":"2019","journal-title":"CoRR"},{"key":"ref14","first-page":"111","article-title":"E–A brainiac theorem prover","volume":"15","author":"schulz","year":"2002","journal-title":"AI Commun"},{"key":"ref15","doi-asserted-by":"crossref","DOI":"10.1038\/nature24270","article-title":"Mastering the game of go without human knowledge","volume":"550","author":"silver","year":"2017","journal-title":"Nature"},{"key":"ref16","first-page":"8836","article-title":"Reinforcement learning of theorem proving","author":"kaliszyk","year":"2018","journal-title":"Proc Int Conf Neural Inf Process"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6\\_23"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-86059-2_10"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_33"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0002-4"},{"key":"ref6","first-page":"29","article-title":"We know (nearly) nothing!","author":"schulz","year":"2017","journal-title":"Proc 1st Int Workshop Automated Reasoning Challenges Appl Directions Exemplary Achievements"},{"key":"ref5","article-title":"The IOA language and toolset: Support for designing, analyzing, and building distributed systems","author":"garland","year":"1998"},{"key":"ref8","first-page":"3084","article-title":"Efficient semantic features for automated reasoning over large theories","author":"kaliszyk","year":"2015","journal-title":"Proc 24th Int Conf Artif Intell"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_23"},{"key":"ref49","article-title":"Layer normalization","author":"ba","year":"2016"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-62075-6_20"},{"key":"ref46","first-page":"593","article-title":"Modeling relational data with graph convolutional networks","author":"schlichtkrull","year":"2018","journal-title":"Proc Eur Semantic Web Conf"},{"key":"ref45","first-page":"2783","article-title":"Premise selection for theorem proving by deep graph embedding","author":"wang","year":"2017"},{"key":"ref48","article-title":"Directed acyclic graph neural networks","author":"thost","year":"0"},{"key":"ref47","article-title":"Improving graph neural network representations of logical formulae with subgraph pooling","author":"crouse","year":"2019"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i03.5689"},{"key":"ref41","article-title":"Reinforced external guidance for theorem provers","author":"rawson","year":"2020"},{"key":"ref44","first-page":"1025","article-title":"Inductive representation learning on large graphs","author":"hamilton","year":"2017"},{"key":"ref43","article-title":"Semi-supervised classification with graph convolutional networks","author":"kipf","year":"2017","journal-title":"Proc 5th Int Conf Learn Representations"}],"container-title":["IEEE Transactions on Pattern Analysis and Machine Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/34\/9970415\/09669114.pdf?arnumber=9669114","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,26]],"date-time":"2022-12-26T19:12:44Z","timestamp":1672081964000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9669114\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,1]]},"references-count":76,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/tpami.2022.3140382","relation":{},"ISSN":["0162-8828","2160-9292","1939-3539"],"issn-type":[{"value":"0162-8828","type":"print"},{"value":"2160-9292","type":"electronic"},{"value":"1939-3539","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,1]]}}}