{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T06:09:34Z","timestamp":1725775774271},"reference-count":44,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,7]]},"DOI":"10.1109\/cec.2016.7744352","type":"proceedings-article","created":{"date-parts":[[2016,11,30]],"date-time":"2016-11-30T22:22:49Z","timestamp":1480544569000},"page":"4421-4428","source":"Crossref","is-referenced-by-count":3,"title":["Automatically proving mathematical theorems with evolutionary algorithms and proof assistants"],"prefix":"10.1109","author":[{"given":"Li-An","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jui-Pin","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao-Hong","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ying-ping","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2006.871253"},{"journal-title":"Linear Genetic Programming Genetic and Evolutionary Computation Series","year":"2007","author":"brameier","key":"ref38"},{"key":"ref33","article-title":"Genetic programming: A paradigm for genetically breeding populations of computer programs to solve problems","author":"koza","year":"1990","journal-title":"Stanford University Stanford CA 94305 Tech Rep STAN-CS-90&#x2013;1314"},{"year":"0","key":"ref32","article-title":"ARM architecture"},{"year":"0","key":"ref31","article-title":"x86"},{"year":"0","key":"ref30","article-title":"GitHub"},{"article-title":"On linear genetic programming","year":"2003","author":"brameier","key":"ref37"},{"key":"ref36","article-title":"Field guide to genetic programming","author":"mcphee","year":"2008","journal-title":"Computer Science Faculty"},{"journal-title":"Genetic Programming An Introduction On the Automatic Evolution of Computer Programs and its Applications","year":"1998","author":"banzhaf","key":"ref35"},{"journal-title":"Genetic Programming On the Programming of Computers by Means of Natural Selection","year":"1992","author":"koza","key":"ref34"},{"journal-title":"The Coq proof assistant reference manual LogiCal Project 2004 version 8 0","year":"0","key":"ref10"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2007.903549"},{"year":"0","key":"ref11","article-title":"The Coq proof assistant"},{"journal-title":"Isabelle\/HOL - A Proof Assistant for Higher-order Logic ser Lecture Notes in Computer Science","year":"0","author":"nipkow","key":"ref12"},{"year":"0","key":"ref13","article-title":"HOL: Interactive theorem prover"},{"year":"0","key":"ref14","article-title":"Isabelle"},{"article-title":"The theory of LEGO: A proof checker for the extended calculus of constructions","year":"1994","author":"pollack","key":"ref15"},{"year":"0","key":"ref16","article-title":"The LEGO proof assistant"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1147\/rd.24.0336"},{"year":"0","key":"ref18","article-title":"Fan Hui"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1038\/529437a"},{"year":"0","key":"ref28","article-title":"Inria - Inventeurs du monde num&#x00E9;rique"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.20.11.584"},{"year":"0","key":"ref27","article-title":"Proof assistant"},{"year":"0","key":"ref3","article-title":"Brouwer-Heyting-Kolmogorov interpretation"},{"year":"0","key":"ref6","article-title":"Curry-Howard correspondence"},{"year":"0","key":"ref29","article-title":"Natural computing laboratory on GitHub"},{"journal-title":"Homotopy Type Theory Univalent Foundations of Mathematics Institute for Advanced Study","year":"2013","key":"ref5"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1238844.1238856"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.2.98"},{"key":"ref2","article-title":"History of constructivism in the twentieth century","author":"troelstra","year":"1991","journal-title":"University of Amsterdam Tech Rep ML-91&#x2013;05"},{"year":"0","key":"ref9","article-title":"Haskell: An advanced purely-functional programming language"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2699407"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1038\/nature16961"},{"year":"0","key":"ref22","article-title":"Lee Sedol"},{"year":"0","key":"ref21","article-title":"AlphaGo"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/TCIAIG.2012.2186810"},{"year":"0","key":"ref24","article-title":"Automated reasoning"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17310-3"},{"key":"ref23","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195099713.001.0001","author":"b\u00e4ck","year":"1996","journal-title":"Evolutionary Algorithms in Theory and Practice Evolution Strategies Evolutionary Programming Genetic Algorithms"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1455567.1455605"},{"key":"ref43","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1145\/36206.36194","article-title":"Superoptimizer: A look at the smallest program","author":"massalin","year":"1987","journal-title":"Proceedings of the second international conference on Architectual support for programming languages and operating systems"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1956.1056797"}],"event":{"name":"2016 IEEE Congress on Evolutionary Computation (CEC)","start":{"date-parts":[[2016,7,24]]},"location":"Vancouver, BC, Canada","end":{"date-parts":[[2016,7,29]]}},"container-title":["2016 IEEE Congress on Evolutionary Computation (CEC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7636124\/7743769\/07744352.pdf?arnumber=7744352","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T22:20:26Z","timestamp":1718922026000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7744352\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7]]},"references-count":44,"URL":"https:\/\/doi.org\/10.1109\/cec.2016.7744352","relation":{},"subject":[],"published":{"date-parts":[[2016,7]]}}}