{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:36:38Z","timestamp":1791459398451,"version":"4.3.4"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1837129"],"award-info":[{"award-number":["CCF-1837129"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-22-9-0063"],"award-info":[{"award-number":["HR0011-22-9-0063"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>Interactive proofs of theorems often require auxiliary helper lemmas to prove the desired theorem. Existing approaches for automatically synthesizing helper lemmas fall into two broad categories. Some approaches are goal-directed, producing lemmas specifically to help a user make progress from a given proof state, but they have limited expressiveness in terms of the lemmas that can be produced. Other approaches are highly expressive, able to generate arbitrary lemmas from a given grammar, but they are completely undirected and hence not amenable to interactive usage.<\/jats:p>\n          <jats:p>In this paper, we develop an approach to lemma synthesis that is both goal-directed and expressive.  \nThe key novelty is a technique for reducing lemma synthesis to a data-driven program synthesis problem, whereby examples for synthesis are generated from the current proof state. We also describe a technique to systematically introduce new variables for lemma synthesis, as well as techniques for filtering and ranking candidate lemmas for presentation to the user. We implement these ideas in a tool called lfind, which can be run as a Coq tactic. In an evaluation on four benchmark suites, lfind produces useful lemmas in 68% of the cases where a human prover used a lemma to make progress. In these cases lfind synthesizes a lemma that either enables a fully automated proof of the original goal or that matches the human-provided lemma.<\/jats:p>","DOI":"10.1145\/3563306","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"505-531","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Data-driven lemma synthesis for interactive proofs"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8074-5517","authenticated-orcid":false,"given":"Aishwarya","family":"Sivaraman","sequence":"first","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0600-7898","authenticated-orcid":false,"given":"Alex","family":"Sanchez-Stern","sequence":"additional","affiliation":[{"name":"University of Massachusetts at Amherst, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0864-0195","authenticated-orcid":false,"given":"Bretton","family":"Chen","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3957-0628","authenticated-orcid":false,"given":"Sorin","family":"Lerner","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2031-1514","authenticated-orcid":false,"given":"Todd","family":"Millstein","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"1995. Circuits. https:\/\/github.com\/coq-contribs\/circuits \t\t\t\t  1995. Circuits. https:\/\/github.com\/coq-contribs\/circuits"},{"key":"e_1_2_1_2_1","unstructured":"2003. Coq-of-Ocaml. https:\/\/github.com\/foobar-land\/coq-of-ocaml \t\t\t\t  2003. Coq-of-Ocaml. https:\/\/github.com\/foobar-land\/coq-of-ocaml"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314641"},{"key":"e_1_2_1_5_1","unstructured":"R Aubin. 1976. Mechanising Structural Induction. \t\t\t\t  R Aubin. 1976. Mechanising Structural Induction."},{"key":"e_1_2_1_6_1","volume-title":"HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version). CoRR, abs\/1904.03241","author":"Bansal Kshitij","year":"2019","unstructured":"Kshitij Bansal , Sarah M. Loos , Markus N. Rabe , Christian Szegedy , and Stewart Wilcox . 2019. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version). CoRR, abs\/1904.03241 ( 2019 ), arxiv:1904.03241. arxiv:1904.03241 Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version). CoRR, abs\/1904.03241 (2019), arxiv:1904.03241. arxiv:1904.03241"},{"key":"e_1_2_1_7_1","volume-title":"Paulson","author":"Blanchette Jasmin Christian","year":"2011","unstructured":"Jasmin Christian Blanchette , Sascha B\u00f6hme , and Lawrence C . Paulson . 2011 . Extending Sledgehammer with SMT Solvers. In Automated Deduction \u2013 CADE-23, Nikolaj Bj\u00f8rner and Viorica Sofronie-Stokkermans (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 116\u2013130. isbn:978-3-642-22438-6 Jasmin Christian Blanchette, Sascha B\u00f6hme, and Lawrence C. Paulson. 2011. Extending Sledgehammer with SMT Solvers. In Automated Deduction \u2013 CADE-23, Nikolaj Bj\u00f8rner and Viorica Sofronie-Stokkermans (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 116\u2013130. isbn:978-3-642-22438-6"},{"key":"e_1_2_1_8_1","series-title":"ACM Monograph Series","volume-title":"A Computational Logic","author":"Boyer Robert S","unstructured":"Robert S Boyer and J Strother Moore . 1979. A Computational Logic . ACM Monograph Series . Robert S Boyer and J Strother Moore. 1979. A Computational Logic. ACM Monograph Series."},{"key":"e_1_2_1_9_1","volume-title":"Andrew Ireland, and Alan Smaill.","author":"Bundy Alan","year":"1993","unstructured":"Alan Bundy , Andrew Stevens , Frank Van Harmelen , Andrew Ireland, and Alan Smaill. 1993 . Rippling : A heuristic for guiding inductive proofs. Artificial intelligence, 62, 2 (1993), 185\u2013253. Alan Bundy, Andrew Stevens, Frank Van Harmelen, Andrew Ireland, and Alan Smaill. 1993. Rippling: A heuristic for guiding inductive proofs. Artificial intelligence, 62, 2 (1993), 185\u2013253."},{"key":"e_1_2_1_10_1","unstructured":"Jacqueline Castaing. 1985. How to Facilitate the Proof of Theorems by Using the Induction-matching and by Generalization. In IJCAI. \t\t\t\t  Jacqueline Castaing. 1985. How to Facilitate the Proof of Theorems by Using the Induction-matching and by Generalization. In IJCAI."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.70.1"},{"key":"e_1_2_1_12_1","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","unstructured":"Adam Chlipala . 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant . MIT Press . Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_14_1","first-page":"38573","volume-title":"USA","volume":"406","author":"Claessen Koen","year":"2013","unstructured":"Koen Claessen , Moa Johansson , Dan Ros\u00e9n , and Nicholas Smallbone . 2013 . Automating Inductive Proofs Using Theory Exploration. In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY , USA , June 9-14, 2013. Proceedings, Maria Paola Bonacina (Ed.) (Lecture Notes in Computer Science , Vol. 7898). Springer, 392\u2013 406 . isbn:978-3-642- 38573 - 38575 Koen Claessen, Moa Johansson, Dan Ros\u00e9n, and Nicholas Smallbone. 2013. Automating Inductive Proofs Using Theory Exploration. In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, Maria Paola Bonacina (Ed.) (Lecture Notes in Computer Science, Vol. 7898). Springer, 392\u2013406. isbn:978-3-642-38573-5"},{"key":"e_1_2_1_15_1","volume-title":"TAP@TOOLS, Gordon Fraser 0001 and Angelo Gargantini (Eds.) (Lecture Notes in Computer Science","author":"Claessen Koen","unstructured":"Koen Claessen , Nicholas Smallbone , and John Hughes . 2010. QuickSpec: Guessing Formal Specifications Using Testing . In TAP@TOOLS, Gordon Fraser 0001 and Angelo Gargantini (Eds.) (Lecture Notes in Computer Science , Vol. 6143). Springer, 6\u2013 21 . isbn:978-3-642-13976-5 Koen Claessen, Nicholas Smallbone, and John Hughes. 2010. QuickSpec: Guessing Formal Specifications Using Testing. In TAP@TOOLS, Gordon Fraser 0001 and Angelo Gargantini (Eds.) (Lecture Notes in Computer Science, Vol. 6143). Springer, 6\u201321. isbn:978-3-642-13976-5"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_2_1_17_1","volume-title":"Automated Deduction - CADE-25, Amy P","author":"de Moura Leonardo","unstructured":"Leonardo de Moura , Soonho Kong , Jeremy Avigad , Floris van Doorn , and Jakob von Raumer . 2015. The Lean Theorem Prover (System Description) . In Automated Deduction - CADE-25, Amy P . Felty and Aart Middeldorp (Eds.). Springer International Publishing , Cham . 378\u2013388. isbn:978-3-319-21401-6 Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham. 378\u2013388. isbn:978-3-319-21401-6"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_22"},{"key":"e_1_2_1_19_1","volume-title":"Dynamically Discovering Likely Program Invariants","author":"Ernst Michael D.","unstructured":"Michael D. Ernst . 2000. Dynamically Discovering Likely Program Invariants . University of Washington Department of Computer Science and Engineering. Seattle , Washington. Michael D. Ernst. 2000. Dynamically Discovering Likely Program Invariants. University of Washington Department of Computer Science and Engineering. Seattle, Washington."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_2_1_22_1","unstructured":"Jean-Christophe Filli\u00e2tre Hugo Herbelin Bruno Barras Bruno Barras Samuel Boutin Eduardo Gim\u00e9nez Samuel Boutin G\u00e9rard Huet C\u00e9sar Mu\u00f1oz Cristina Cornes Cristina Cornes Judica\u00ebl Courant Judicael Courant Chetan Murthy Chetan Murthy Catherine Parent Catherine Parent Christine Paulin-mohring Christine Paulin-mohring Amokrane Saibi Amokrane Saibi Benjamin Werner and Benjamin Werner. 1997. The Coq Proof Assistant - Reference Manual Version 6.1. \t\t\t\t  Jean-Christophe Filli\u00e2tre Hugo Herbelin Bruno Barras Bruno Barras Samuel Boutin Eduardo Gim\u00e9nez Samuel Boutin G\u00e9rard Huet C\u00e9sar Mu\u00f1oz Cristina Cornes Cristina Cornes Judica\u00ebl Courant Judicael Courant Chetan Murthy Chetan Murthy Catherine Parent Catherine Parent Christine Paulin-mohring Christine Paulin-mohring Amokrane Saibi Amokrane Saibi Benjamin Werner and Benjamin Werner. 1997. The Coq Proof Assistant - Reference Manual Version 6.1."},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Emily First Yuriy Brun and Arjun Guha. 2020. TacTok: Semantics-Aware Proof Synthesis. In Object-oriented Programming Systems Languages and Applications. \t\t\t\t  Emily First Yuriy Brun and Arjun Guha. 2020. TacTok: Semantics-Aware Proof Synthesis. In Object-oriented Programming Systems Languages and Applications.","DOI":"10.1145\/3428299"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837629"},{"key":"e_1_2_1_25_1","unstructured":"Emilio Jes\u00fas Gallego Arias Karl Palmskog and Vasily Pestun. 2020. SerAPI:Machine-Friendly Data-Centric Serialization for Coq. https:\/\/github.com\/ejgallego\/coq-serapi \t\t\t\t  Emilio Jes\u00fas Gallego Arias Karl Palmskog and Vasily Pestun. 2020. SerAPI:Machine-Friendly Data-Centric Serialization for Coq. https:\/\/github.com\/ejgallego\/coq-serapi"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.29007\/ntlb"},{"key":"e_1_2_1_29_1","first-page":"45220","volume-title":"Stellenbosch","volume":"406","author":"Heras J\u00f3nathan","year":"2013","unstructured":"J\u00f3nathan Heras , Ekaterina Komendantskaya , Moa Johansson , and Ewen Maclean . 2013 . Proof-Pattern Recognition and Lemma Discovery in ACL2. In Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19 , Stellenbosch , South Africa , December 14-19, 2013. Proceedings, Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov (Eds.) (Lecture Notes in Computer Science, Vol. 8312). Springer, 389\u2013 406 . isbn:978-3-642- 45220 - 45228 J\u00f3nathan Heras, Ekaterina Komendantskaya, Moa Johansson, and Ewen Maclean. 2013. Proof-Pattern Recognition and Lemma Discovery in ACL2. In Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov (Eds.) (Lecture Notes in Computer Science, Vol. 8312). Springer, 389\u2013406. isbn:978-3-642-45220-8"},{"key":"e_1_2_1_31_1","volume-title":"GamePad: A Learning Environment for Theorem Proving. In 7th International Conference on Learning Representations, ICLR 2019","author":"Huang Daniel","year":"2019","unstructured":"Daniel Huang , Prafulla Dhariwal , Dawn Song , and Ilya Sutskever . 2019 . GamePad: A Learning Environment for Theorem Proving. In 7th International Conference on Learning Representations, ICLR 2019 , New Orleans, LA, USA , May 6-9, 2019. OpenReview.net. https:\/\/openreview.net\/forum?id=r1xwKoR9Y7 Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. 2019. GamePad: A Learning Environment for Theorem Proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net. https:\/\/openreview.net\/forum?id=r1xwKoR9Y7"},{"key":"e_1_2_1_32_1","unstructured":"B Hummel. 1990. Generation of induction axioms and generalisation. \t\t\t\t  B Hummel. 1990. Generation of induction axioms and generalisation."},{"key":"e_1_2_1_33_1","volume-title":"Automated Mathematical Induction","author":"Ireland Andrew","unstructured":"Andrew Ireland and Alan Bundy . 1996. Productive use of failure in inductive proof . In Automated Mathematical Induction . Springer , 79\u2013111. Andrew Ireland and Alan Bundy. 1996. Productive use of failure in inductive proof. In Automated Mathematical Induction. Springer, 79\u2013111."},{"key":"e_1_2_1_34_1","first-page":"23250","volume-title":"CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings, Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen (Eds.) (Lecture Notes in Computer Science","volume":"139","author":"Johansson Moa","year":"2019","unstructured":"Moa Johansson . 2019 . Lemma Discovery for Induction - A Survey. In Intelligent Computer Mathematics - 12th International Conference , CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings, Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen (Eds.) (Lecture Notes in Computer Science , Vol. 11617). Springer, 125\u2013 139 . isbn:978-3-030-23249-8; 978-3-030- 23250 - 23254 Moa Johansson. 2019. Lemma Discovery for Induction - A Survey. In Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings, Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen (Eds.) (Lecture Notes in Computer Science, Vol. 11617). Springer, 125\u2013139. isbn:978-3-030-23249-8; 978-3-030-23250-4"},{"key":"e_1_2_1_35_1","first-page":"17171","volume-title":"Simon Siegler and Nathan Wasser (Eds.) (Lecture Notes in Computer Science","volume":"116","author":"Johansson Moa","year":"2010","unstructured":"Moa Johansson , Lucas Dixon , and Alan Bundy . 2010 . Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery. In Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday , Simon Siegler and Nathan Wasser (Eds.) (Lecture Notes in Computer Science , Vol. 6463). Springer, 102\u2013 116 . isbn:978-3-642- 17171 - 17170 Moa Johansson, Lucas Dixon, and Alan Bundy. 2010. Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery. In Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday, Simon Siegler and Nathan Wasser (Eds.) (Lecture Notes in Computer Science, Vol. 6463). Springer, 102\u2013116. isbn:978-3-642-17171-0"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9193-y"},{"key":"e_1_2_1_37_1","volume-title":"Hipster: Integrating Theory Exploration in a Proof Assistant. In Intelligent Computer Mathematics - International Conference, CICM","author":"Johansson Moa","year":"2014","unstructured":"Moa Johansson , Dan Ros\u00e9n , Nicholas Smallbone , and Koen Claessen . 2014 . Hipster: Integrating Theory Exploration in a Proof Assistant. In Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings, Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, and Josef Urban (Eds.) (Lecture Notes in Computer Science , Vol. 8543). Springer, 108\u2013 122 . isbn:978-3-319-08433-6 Moa Johansson, Dan Ros\u00e9n, Nicholas Smallbone, and Koen Claessen. 2014. Hipster: Integrating Theory Exploration in a Proof Assistant. In Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings, Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, and Josef Urban (Eds.) (Lecture Notes in Computer Science, Vol. 8543). Springer, 108\u2013122. isbn:978-3-319-08433-6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0182-0"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9330-8"},{"key":"e_1_2_1_40_1","first-page":"61511","volume-title":"13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, Michael A. McRobbie and John K. Slaney (Eds.) (Lecture Notes in Computer Science","volume":"552","author":"Kapur Deepak","year":"1996","unstructured":"Deepak Kapur and Mahadevan Subramaniam . 1996 . Lemma Discovery in Automated Induction. In Automated Deduction - CADE-13 , 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, Michael A. McRobbie and John K. Slaney (Eds.) (Lecture Notes in Computer Science , Vol. 1104). Springer, 538\u2013 552 . isbn:3-540- 61511 - 61513 Deepak Kapur and Mahadevan Subramaniam. 1996. Lemma Discovery in Automated Induction. In Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, Michael A. McRobbie and John K. Slaney (Eds.) (Lecture Notes in Computer Science, Vol. 1104). Springer, 538\u2013552. isbn:3-540-61511-3"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408991"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498682"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2011.06.055"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2738007"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i03.5689"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523707"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"e_1_2_1_51_1","volume-title":"Natural Deduction as Higher-Order Resolution. CoRR, cs.LO\/9301104","author":"Paulson Lawrence C.","year":"1993","unstructured":"Lawrence C. Paulson . 1993. Natural Deduction as Higher-Order Resolution. CoRR, cs.LO\/9301104 ( 1993 ), arxiv:cs.LO\/9301104 Lawrence C. Paulson. 1993. Natural Deduction as Higher-Order Resolution. CoRR, cs.LO\/9301104 (1993), arxiv:cs.LO\/9301104"},{"key":"e_1_2_1_52_1","volume-title":"VMCAI, Deepak D\u2019Souza, Akash Lal, and Kim Guldstrand Larsen (Eds.) (Lecture Notes in Computer Science","author":"Reynolds Andrew","unstructured":"Andrew Reynolds and Viktor Kuncak . 2015. Induction for SMT Solvers . In VMCAI, Deepak D\u2019Souza, Akash Lal, and Kim Guldstrand Larsen (Eds.) (Lecture Notes in Computer Science , Vol. 8931). Springer, 80\u2013 98 . isbn:978-3-662-46080-1 Andrew Reynolds and Viktor Kuncak. 2015. Induction for SMT Solvers. In VMCAI, Deepak D\u2019Souza, Akash Lal, and Kim Guldstrand Larsen (Eds.) (Lecture Notes in Computer Science, Vol. 8931). Springer, 80\u201398. isbn:978-3-662-46080-1"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3394450.3397466"},{"key":"e_1_2_1_54_1","volume-title":"Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic. CoRR, abs\/1706.06462","author":"Sekiyama Taro","year":"2017","unstructured":"Taro Sekiyama , Akifumi Imanishi , and Kohei Suenaga . 2017. Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic. CoRR, abs\/1706.06462 ( 2017 ), arxiv:1706.06462. arxiv:1706.06462 Taro Sekiyama, Akifumi Imanishi, and Kohei Suenaga. 2017. Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic. CoRR, abs\/1706.06462 (2017), arxiv:1706.06462. arxiv:1706.06462"},{"key":"e_1_2_1_55_1","first-page":"10671","volume-title":"7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, Zhenjiang Hu (Ed.) (Lecture Notes in Computer Science","volume":"13","author":"Solar-Lezama Armando","year":"2009","unstructured":"Armando Solar-Lezama . 2009 . The Sketching Approach to Program Synthesis. In Programming Languages and Systems , 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, Zhenjiang Hu (Ed.) (Lecture Notes in Computer Science , Vol. 5904). Springer, 4\u2013 13 . isbn:978-3-642- 10671 - 10672 Armando Solar-Lezama. 2009. The Sketching Approach to Program Synthesis. In Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, Zhenjiang Hu (Ed.) (Lecture Notes in Computer Science, Vol. 5904). Springer, 4\u201313. isbn:978-3-642-10671-2"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_28"},{"key":"e_1_2_1_57_1","unstructured":"Daniel Whalen. 2016. Holophrasm: a neural Automated Theorem Prover for higher-order logic. arxiv:1608.02644. \t\t\t\t  Daniel Whalen. 2016. Holophrasm: a neural Automated Theorem Prover for higher-order logic. arxiv:1608.02644."},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the 36th International Conference on Machine Learning, ICML 2019","volume":"6994","author":"Yang Kaiyu","year":"2019","unstructured":"Kaiyu Yang and Jia Deng . 2019 . Learning to Prove Theorems via Interacting with Proof Assistants . In Proceedings of the 36th International Conference on Machine Learning, ICML 2019 , 9-15 June 2019, Long Beach, California, USA, Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.) (Proceedings of Machine Learning Research , Vol. 97). PMLR, 6984\u2013 6994 . http:\/\/proceedings.mlr.press\/v97\/yang19a.html Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Interacting with Proof Assistants. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.) (Proceedings of Machine Learning Research, Vol. 97). PMLR, 6984\u20136994. http:\/\/proceedings.mlr.press\/v97\/yang19a.html"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30048-7_35"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192416"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563306","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563306","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563306","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563306"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":59,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563306"],"URL":"https:\/\/doi.org\/10.1145\/3563306","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}