{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:50:49Z","timestamp":1782877849628,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,9,3]],"date-time":"2018-09-03T00:00:00Z","timestamp":1535932800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","award":["CZ.02.1.01\/0.0\/0.0\/15_003\/0000466"],"award-info":[{"award-number":["CZ.02.1.01\/0.0\/0.0\/15_003\/0000466"]}],"id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,9,3]]},"DOI":"10.1145\/3238147.3238210","type":"proceedings-article","created":{"date-parts":[[2018,8,20]],"date-time":"2018-08-20T20:04:36Z","timestamp":1534795476000},"page":"362-372","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["PaMpeR: proof method recommendation system for Isabelle\/HOL"],"prefix":"10.1145","author":[{"given":"Yutaka","family":"Nagashima","sequence":"first","affiliation":[{"name":"Czech Technical University, Czechia \/ University of Innsbruck, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yilun","family":"He","sequence":"additional","affiliation":[{"name":"University of Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,9,3]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"PSL with PGT: CICM2018 for Isabelle2017. (2018","year":"2018","unstructured":"2018. PSL with PGT: CICM2018 for Isabelle2017. (2018 ). https:\/\/github. com\/data61\/PSL\/releases\/tag\/v0.1.1 To use PaMpeR, one first needs to install Isabelle\/HOL, which is distributed at https:\/\/isabelle.in.tum.de\/. PaMpeR: Proof Method Recommendation System for Isabelle\/HOL ASE \u201918, September 3\u20137 , 2018 , Montpellier, France 2018. PSL with PGT: CICM2018 for Isabelle2017. (2018). https:\/\/github. com\/data61\/PSL\/releases\/tag\/v0.1.1 To use PaMpeR, one first needs to install Isabelle\/HOL, which is distributed at https:\/\/isabelle.in.tum.de\/. PaMpeR: Proof Method Recommendation System for Isabelle\/HOL ASE \u201918, September 3\u20137, 2018, Montpellier, France"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"e_1_3_2_1_3_1","unstructured":"Springer 3\u201317.  Springer 3\u201317."},{"key":"e_1_3_2_1_4_1","unstructured":"Leo Breiman J. H. Friedman R. A. Olshen and C. J. Stone. 1984. Classification and Regression Trees. Wadsworth.  Leo Breiman J. H. Friedman R. A. Olshen and C. J. Stone. 1984. Classification and Regression Trees. Wadsworth."},{"key":"e_1_3_2_1_5_1","volume-title":"21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun","volume":"46","author":"Gauthier Thibault","year":"2017","unstructured":"Thibault Gauthier , Cezary Kaliszyk , and Josef Urban . 2017 . TacticToe: Learning to Reason with HOL4 Tactics. In LPAR-21 , 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun , Botswana, May 7-12, 2017 (EPiC Series in Computing), Thomas Eiter and David Sands (Eds.) , Vol. 46 . EasyChair, 125\u2013143. http:\/\/www.easychair.org\/publications\/paper\/340355 Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. 2017. TacticToe: Learning to Reason with HOL4 Tactics. In LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017 (EPiC Series in Computing), Thomas Eiter and David Sands (Eds.), Vol. 46. EasyChair, 125\u2013143. http:\/\/www.easychair.org\/publications\/paper\/340355"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"e_1_3_2_1_7_1","unstructured":"Thomas C. Hales Mark Adams Gertrud Bauer Dat Tat Dang John Harrison Truong Le Hoang Cezary Kaliszyk Victor Magron Sean McLaughlin Thang Tat Nguyen Truong Quang Nguyen Tobias Nipkow Steven Obua Joseph Pleso Jason M. Rute Alexey Solovyev An Hoai Thi Ta Trung Nam Tran Diep Thi Trieu Josef Urban Ky Khac Vu and Roland Zumkeller. 2015. A formal proof of the Kepler conjecture. CoRR abs\/1501.02155 (2015). arXiv: 1501.02155 http: \/\/arxiv.org\/abs\/1501.02155  Thomas C. Hales Mark Adams Gertrud Bauer Dat Tat Dang John Harrison Truong Le Hoang Cezary Kaliszyk Victor Magron Sean McLaughlin Thang Tat Nguyen Truong Quang Nguyen Tobias Nipkow Steven Obua Joseph Pleso Jason M. Rute Alexey Solovyev An Hoai Thi Ta Trung Nam Tran Diep Thi Trieu Josef Urban Ky Khac Vu and Roland Zumkeller. 2015. A formal proof of the Kepler conjecture. CoRR abs\/1501.02155 (2015). arXiv: 1501.02155 http: \/\/arxiv.org\/abs\/1501.02155"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2008.239"},{"key":"e_1_3_2_1_9_1","unstructured":"2008.239  2008.239"},{"key":"e_1_3_2_1_10_1","volume-title":"ML4PG: proof-mining in Coq. CoRR abs\/1302.6421","author":"Heras J\u00f3nathan","year":"2013","unstructured":"J\u00f3nathan Heras and Ekaterina Komendantskaya . 2013. ML4PG: proof-mining in Coq. CoRR abs\/1302.6421 ( 2013 ). arXiv: 1302.6421 http:\/\/arxiv.org\/abs\/1302.6421 J\u00f3nathan Heras and Ekaterina Komendantskaya. 2013. ML4PG: proof-mining in Coq. CoRR abs\/1302.6421 (2013). arXiv: 1302.6421 http:\/\/arxiv.org\/abs\/1302.6421"},{"key":"e_1_3_2_1_11_1","volume-title":"DeepMath - Deep Sequence Models for Premise Selection. In Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016","author":"Irving Geoffrey","year":"2016","unstructured":"Geoffrey Irving , Christian Szegedy , Alexander A. Alemi , Niklas E\u00e9n , Fran\u00e7ois Chollet , and Josef Urban . 2016 . DeepMath - Deep Sequence Models for Premise Selection. In Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016 , December 5-10, 2016, Barcelona, Spain, Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett (Eds.). 2235\u20132243. http:\/\/papers.nips.cc\/paper\/ 6280-deepmath-deep-sequence-models-for-premise-selection Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas E\u00e9n, Fran\u00e7ois Chollet, and Josef Urban. 2016. DeepMath - Deep Sequence Models for Premise Selection. In Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett (Eds.). 2235\u20132243. http:\/\/papers.nips.cc\/paper\/ 6280-deepmath-deep-sequence-models-for-premise-selection"},{"key":"e_1_3_2_1_12_1","unstructured":"Gareth James Daniela Witten Trevor Hastie and Robert Tibshirani. {n. d.}. An Introduction to Statistical Learning.   Gareth James Daniela Witten Trevor Hastie and Robert Tibshirani. {n. d.}. An Introduction to Statistical Learning."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_14_1","unstructured":"Gerwin Klein Tobias Nipkow Larry Paulson and Rene Thiemann. {n. d.}.. https:\/\/www.isa-afp.org\/  Gerwin Klein Tobias Nipkow Larry Paulson and Rene Thiemann. {n. d.}.. https:\/\/www.isa-afp.org\/"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_6"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_18_1","volume-title":"21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun","volume":"46","author":"Loos Sarah M.","year":"2017","unstructured":"Sarah M. Loos , Geoffrey Irving , Christian Szegedy , and Cezary Kaliszyk . 2017 . Deep Network Guided Proof Search. In LPAR-21 , 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun , Botswana, May 7-12, 2017 (EPiC Series in Computing), Thomas Eiter and David Sands (Eds.) , Vol. 46 . EasyChair, 85\u2013105. http:\/\/www.easychair.org\/publications\/paper\/340345 Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. 2017. Deep Network Guided Proof Search. In LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017 (EPiC Series in Computing), Thomas Eiter and David Sands (Eds.), Vol. 46. EasyChair, 85\u2013105. http:\/\/www.easychair.org\/publications\/paper\/340345"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2818754.2818842"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2007.07.004"},{"key":"e_1_3_2_1_21_1","volume-title":"PaMpeR: Proof Method Recommendation System for Isabelle\/HOL. CoRR abs\/1806.07239","author":"Nagashima Yutaka","year":"2018","unstructured":"Yutaka Nagashima and Yilun He. 2018. PaMpeR: Proof Method Recommendation System for Isabelle\/HOL. CoRR abs\/1806.07239 ( 2018 ). arXiv: 1806.07239 http: \/\/arxiv.org\/abs\/1806.07239 Yutaka Nagashima and Yilun He. 2018. PaMpeR: Proof Method Recommendation System for Isabelle\/HOL. CoRR abs\/1806.07239 (2018). arXiv: 1806.07239 http: \/\/arxiv.org\/abs\/1806.07239"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_32"},{"key":"e_1_3_2_1_23_1","volume-title":"Lecture Notes in Computer Science","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2002. Isabelle\/ HOL - A Proof Assistant for Higher-Order Logic . Lecture Notes in Computer Science , Vol. 2283 . Springer . Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9322-8"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1953048.2078195"}],"event":{"name":"ASE '18: 33rd ACM\/IEEE International Conference on Automated Software Engineering","location":"Montpellier France","acronym":"ASE '18","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","CNRS Centre National De La Rechercue Scientifique","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE-CS Computer Society"]},"container-title":["Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3238147.3238210","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3238147.3238210","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:35Z","timestamp":1750210775000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3238147.3238210"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,3]]},"references-count":25,"alternative-id":["10.1145\/3238147.3238210","10.1145\/3238147"],"URL":"https:\/\/doi.org\/10.1145\/3238147.3238210","relation":{},"subject":[],"published":{"date-parts":[[2018,9,3]]},"assertion":[{"value":"2018-09-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}