{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:06:58Z","timestamp":1770271618818,"version":"3.49.0"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:p>We present sem_ind, a recommendation tool for proof by induction in Isabelle\/HOL.\n\nGiven an inductive problem, sem_ind produces candidate arguments for proof by induction, and selects promising ones using heuristics.\n\nOur evaluation based on 1,095 inductive problems from 22 source files shows that sem_ind improves the accuracy of recommendation from 20.1% to 38.2% for the most promising candidates within 5.0 seconds of timeout compared to its predecessor while decreasing the median value of execution time from 2.79 seconds to 1.06 seconds.<\/jats:p>","DOI":"10.24963\/ijcai.2021\/273","type":"proceedings-article","created":{"date-parts":[[2021,8,11]],"date-time":"2021-08-11T11:00:49Z","timestamp":1628679649000},"page":"1981-1988","source":"Crossref","is-referenced-by-count":6,"title":["Faster Smarter Proof by Induction in Isabelle\/HOL"],"prefix":"10.24963","author":[{"given":"Yutaka","family":"Nagashima","sequence":"first","affiliation":[{"name":"Yale-NUS College, National University of Singapore"},{"name":"University of Innsbruck"},{"name":"Czech Institute of Informatics, Robotics, and Cybernetics, Czech Technical University in Prague"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"name":"Thirtieth International Joint Conference on Artificial Intelligence {IJCAI-21}","theme":"Artificial Intelligence","location":"Montreal, Canada","acronym":"IJCAI-2021","number":"30","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)"],"start":{"date-parts":[[2021,8,19]]},"end":{"date-parts":[[2021,8,27]]}},"container-title":["Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2021,8,11]],"date-time":"2021-08-11T11:02:22Z","timestamp":1628679742000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2021\/273"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2021\/273","relation":{},"subject":[],"published":{"date-parts":[[2021,8]]}}}