{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T03:24:52Z","timestamp":1648783492378},"reference-count":15,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.342.7","type":"journal-article","created":{"date-parts":[[2021,9,6]],"date-time":"2021-09-06T17:02:25Z","timestamp":1630947745000},"page":"78-85","source":"Crossref","is-referenced-by-count":0,"title":["Learned Provability Likelihood for Tactical Search"],"prefix":"10.4204","volume":"342","author":[{"given":"Thibault","family":"Gauthier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"2720","published-online":{"date-parts":[[2021,9,6]]},"reference":[{"key":"DBLP:conf\/pkdd\/AugerCT13","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-40988-2_13","article-title":"Continuous Upper Confidence Trees with Polynomial Exploration - Consistency","volume-title":"Machine Learning and Knowledge Discovery in Databases - European Conference, ECML PKDD 2013, Prague, Czech Republic, September 23-27, 2013, Proceedings, Part I","author":"Auger","year":"2013"},{"key":"DBLP:conf\/icml\/BansalLRSW19","series-title":"Proceedings of Machine Learning Research","first-page":"454","article-title":"HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving","volume-title":"Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA","volume":"97","author":"Bansal","year":"2019"},{"key":"coq","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-540-71067-7_3","article-title":"A Short Presentation of Coq","volume-title":"Conference on Theorem Proving in Higher Order Logics (TPHOLs)","volume":"5170","author":"Bertot","year":"2008"},{"key":"DBLP:conf\/mkm\/BlaauwbroekUG20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-030-53518-6_17","article-title":"The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq","volume-title":"Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings","volume":"12236","author":"Blaauwbroek","year":"2020"},{"key":"DBLP:conf\/cade\/ChvalovskyJ0U19","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-030-29436-6_12","article-title":"ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E","volume-title":"Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings","author":"Chvalovsk\u00fd","year":"2019"},{"key":"DBLP:conf\/lpar\/Gauthier20","series-title":"EPiC Series in Computing","doi-asserted-by":"publisher","first-page":"230","DOI":"10.29007\/7jmg","article-title":"Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic","volume-title":"LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020","volume":"73","author":"Gauthier","year":"2020"},{"key":"DBLP:conf\/mkm\/Gauthier20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-030-53518-6_18","article-title":"Tree Neural Networks in HOL4","volume-title":"Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings","volume":"12236","author":"Gauthier","year":"2020"},{"issue":"2","key":"DBLP:journals\/jar\/GauthierKUKN21","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10817-020-09580-x","article-title":"TacticToe: Learning to Prove with Tactics","volume":"65","author":"Gauthier","year":"2021","journal-title":"J. Autom. Reason."},{"key":"hollight","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","article-title":"HOL Light: An Overview","volume-title":"Conference on Theorem Proving in Higher Order Logics (TPHOLs)","volume":"5674","author":"Harrison","year":"2009"},{"key":"hurd05","first-page":"103","article-title":"System Description: The Metis Proof Tactic","volume-title":"Workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL)","author":"Hurd","year":"2005"},{"key":"DBLP:conf\/nips\/KaliszykUMO18","first-page":"8836","article-title":"Reinforcement Learning of Theorem Proving","volume-title":"Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada","author":"Kaliszyk","year":"2018"},{"key":"DBLP:conf\/kbse\/NagashimaH18","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/3238147.3238210","article-title":"PaMpeR: proof method recommendation system for Isabelle\/HOL","volume-title":"Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018","author":"Nagashima","year":"2018"},{"key":"silver2017mastering","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1038\/nature24270","article-title":"Mastering the game of Go without human knowledge","volume":"550","author":"Silver","year":"2017","journal-title":"Nature"},{"key":"hol4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","article-title":"A Brief Overview of HOL4","volume-title":"Conference on Theorem Proving in Higher Order Logics (TPHOLs)","volume":"5170","author":"Slind","year":"2008"},{"key":"isabelle","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71067-7_7","article-title":"The Isabelle Framework","volume-title":"Conference on Theorem Proving in Higher Order Logics (TPHOLs)","volume":"5170","author":"Wenzel","year":"2008"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2021,9,15]],"date-time":"2021-09-15T01:29:11Z","timestamp":1631669351000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2109.03234v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,6]]},"references-count":15,"URL":"https:\/\/doi.org\/10.4204\/eptcs.342.7","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9,6]]}}}