{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:29:19Z","timestamp":1750220959494,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,3,30]],"date-time":"2020-03-30T00:00:00Z","timestamp":1585526400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,3,30]]},"DOI":"10.1145\/3341105.3373917","type":"proceedings-article","created":{"date-parts":[[2020,3,29]],"date-time":"2020-03-29T12:13:52Z","timestamp":1585484032000},"page":"513-520","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Proof searching in HOL4 with genetic algorithm"],"prefix":"10.1145","author":[{"given":"M. Zohaib","family":"Nawaz","sequence":"first","affiliation":[{"name":"National University of Sciences and Technology, Islamabad, Pakistan"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[{"name":"National University of Sciences and Technology, Islamabad, Pakistan"}]},{"given":"M. Saqib","family":"Nawaz","sequence":"additional","affiliation":[{"name":"Harbin Institute of Technology, Shenzhen, China"}]},{"given":"Philippe","family":"Fournier-Viger","sequence":"additional","affiliation":[{"name":"Harbin Institute of Technology, Shenzhen, China"}]},{"given":"Meng","family":"Sun","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}]}],"member":"320","published-online":{"date-parts":[[2020,3,30]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Y. Bertot and P. Casteran. 2003. Interactive theorem proving and program development: Coq'Art: The calculus of inductive construction. Springer.  Y. Bertot and P. Casteran. 2003. Interactive theorem proving and program development: Coq'Art: The calculus of inductive construction. Springer."},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of IJCAR","volume":"9706","author":"F\u00e4rber M.","year":"2016","unstructured":"M. F\u00e4rber and C. E. Brown . 2016. Internal guidance for Satallax . In Proceedings of IJCAR , 2016 (LNCS), Vol. 9706 . Springer, 349--361. M. F\u00e4rber and C. E. Brown. 2016. Internal guidance for Satallax. In Proceedings of IJCAR, 2016 (LNCS), Vol. 9706. Springer, 349--361."},{"issue":"1","key":"e_1_3_2_1_4_1","first-page":"54","article-title":"2017. A survey of sequential pattern mining","volume":"1","author":"Fournier-Viger P.","year":"2017","unstructured":"P. Fournier-Viger , J. C. W. Lin , R. U. Kiran , Y. S. Koh , and R. Thomas . 2017. A survey of sequential pattern mining . Data Science and Pattern Recognition 1 ( 1 ) ( 2017 ), 54 -- 77 . P. Fournier-Viger, J. C. W. Lin, R. U. Kiran, Y. S. Koh, and R. Thomas. 2017. A survey of sequential pattern mining. Data Science and Pattern Recognition 1(1) (2017), 54--77.","journal-title":"Data Science and Pattern Recognition"},{"key":"e_1_3_2_1_5_1","unstructured":"GA implementation. [n.d.]. Available at: github.com\/muhammadzohaibnawaz\/GAHOL4.  GA implementation. [n.d.]. Available at: github.com\/muhammadzohaibnawaz\/GAHOL4."},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of LPAR","volume":"46","author":"Gauthier T.","year":"2017","unstructured":"T. Gauthier , C. Kaliszyk , and J. Urban . 2017. TacticToe: Learning to reason with HOL4 tactics . In Proceedings of LPAR , 2017 (EPiC Series in Computing) , Vol. 46 . 125--143. T. Gauthier, C. Kaliszyk, and J. Urban. 2017. TacticToe: Learning to reason with HOL4 tactics. In Proceedings of LPAR, 2017 (EPiC Series in Computing), Vol. 46. 125--143."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"O. Hasan and S. Tahar. 2015. Formal verification methods. In Encyclopedia of Information Science & Technology 3rd edition. IGI Global 7162--7170.  O. Hasan and S. Tahar. 2015. Formal verification methods. In Encyclopedia of Information Science & Technology 3rd edition. IGI Global 7162--7170.","DOI":"10.4018\/978-1-4666-5888-2.ch705"},{"volume-title":"Adaptation in natural and artificial systems","author":"Holland J. H.","key":"e_1_3_2_1_8_1","unstructured":"J. H. Holland . 1975. Adaptation in natural and artificial systems . University of Michigan Press , Ann Arbor, MI, USA . J. H. Holland. 1975. Adaptation in natural and artificial systems. University of Michigan Press, Ann Arbor, MI, USA."},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of CEC","author":"Huang S. Y.","year":"2017","unstructured":"S. Y. Huang and Y. P. Chen . 2017. Proving theorems by using evolutionary search with human involvement . In Proceedings of CEC , 2017 . IEEE, 1495--1502. S. Y. Huang and Y. P. Chen. 2017. Proving theorems by using evolutionary search with human involvement. In Proceedings of CEC, 2017. IEEE, 1495--1502."},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of NIPS","author":"Irving G.","year":"2016","unstructured":"G. Irving , C. Szegedy , A. A. Alemi , N. E\u00e9n , F. Chollet , and J. Urban . 2016. DeepMath - Deep sequence models for premise selection . In Proceedings of NIPS , 2016 . ACM, 2235--2243. G. Irving, C. Szegedy, A. A. Alemi, N. E\u00e9n, F. Chollet, and J. Urban. 2016. DeepMath - Deep sequence models for premise selection. In Proceedings of NIPS, 2016. ACM, 2235--2243."},{"key":"e_1_3_2_1_11_1","unstructured":"C. Kaliszyk F. Chollet and C. Szegedy. 2017. HolStep: A machine learning dataset for Higher-Order Logic theorem proving. CoRR abs\/1703.00426 (2017).  C. Kaliszyk F. Chollet and C. Szegedy. 2017. HolStep: A machine learning dataset for Higher-Order Logic theorem proving. CoRR abs\/1703.00426 (2017)."},{"key":"e_1_3_2_1_12_1","volume-title":"Machine Learning of Coq Proof Guidance: First Experiments. In Proceedings of SCSS","volume":"30","author":"Kaliszyk C.","year":"2014","unstructured":"C. Kaliszyk , L. Mamane , and J. Urban . 2014 . Machine Learning of Coq Proof Guidance: First Experiments. In Proceedings of SCSS , 2014 (EPiC Series in Computing) , Vol. 30 . 27--34. C. Kaliszyk, L. Mamane, and J. Urban. 2014. Machine Learning of Coq Proof Guidance: First Experiments. In Proceedings of SCSS, 2014 (EPiC Series in Computing), Vol. 30. 27--34."},{"volume-title":"Genetic programming - On the programming of computers by means of natural selection","author":"Koza J. R.","key":"e_1_3_2_1_13_1","unstructured":"J. R. Koza . 1993. Genetic programming - On the programming of computers by means of natural selection . MIT Press . J. R. Koza. 1993. Genetic programming - On the programming of computers by means of natural selection. MIT Press."},{"volume-title":"An introduction to genetic algorithms","author":"Mitchell M.","key":"e_1_3_2_1_14_1","unstructured":"M. Mitchell . 1996. An introduction to genetic algorithms . MIT Press . M. Mitchell. 1996. An introduction to genetic algorithms. MIT Press."},{"key":"e_1_3_2_1_15_1","first-page":"03028","article-title":"2019. A survey on theorem provers in Formal methods. arXiv:cs.","author":"Nawaz M. S.","year":"1912","unstructured":"M. S. Nawaz , M. Malik , Y. Li , M. Sun , and M. I. Lali . 2019. A survey on theorem provers in Formal methods. arXiv:cs. SE\/ 1912 . 03028 . M. S. Nawaz, M. Malik, Y. Li, M. Sun, and M. I. Lali. 2019. A survey on theorem provers in Formal methods. arXiv:cs.SE\/1912.03028.","journal-title":"SE\/"},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of BDIOT","author":"Nawaz M. S.","year":"2018","unstructured":"M. S. Nawaz and M. Sun . 2018. A formal design model for genetic algorithms operators and its encoding in PVS . In Proceedings of BDIOT , 2018 . ACM, 186--190. M. S. Nawaz and M. Sun. 2018. A formal design model for genetic algorithms operators and its encoding in PVS. In Proceedings of BDIOT, 2018. ACM, 186--190."},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of FSEN","volume":"11761","author":"Nawaz M. S.","year":"2019","unstructured":"M. S. Nawaz , M. Sun , and P. Fournier-Viger . 2019. Proof guidance in PVS with sequential pattern mining . In Proceedings of FSEN , 2019 (LNCS), Vol. 11761 . Springer, 45--60. M. S. Nawaz, M. Sun, and P. Fournier-Viger. 2019. Proof guidance in PVS with sequential pattern mining. In Proceedings of FSEN, 2019 (LNCS), Vol. 11761. Springer, 45--60."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejor.2006.02.012"},{"key":"e_1_3_2_1_19_1","author":"Owre S.","year":"2001","unstructured":"S. Owre , N. Shankar , J. M. Rushby , and D. W . J. Stringer-Calvert. 2001 . PVS system guide, PVS prover guide, PVS language reference. Technical Report. SRI International. S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. 2001. PVS system guide, PVS prover guide, PVS language reference. Technical Report. SRI International.","journal-title":"J. Stringer-Calvert."},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of TLCA","volume":"38","author":"Santo J. E.","year":"2015","unstructured":"J. E. Santo . 2015 . Curry-Howard for sequent calculus at last! . In Proceedings of TLCA , 2015 (LIPIcs), Vol. 38 . 165--179. J. E. Santo. 2015. Curry-Howard for sequent calculus at last!. In Proceedings of TLCA, 2015 (LIPIcs), Vol. 38. 165--179."},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of TPHOL","author":"Slind K.","year":"2008","unstructured":"K. Slind and M. Norrish . 2008. A brief overview of HOL4 . In Proceedings of TPHOL , 2008 . Springer, 28--32. K. Slind and M. Norrish. 2008. A brief overview of HOL4. In Proceedings of TPHOL, 2008. Springer, 28--32."},{"key":"e_1_3_2_1_22_1","first-page":"4421","article-title":"2016. Automatically proving mathematical theorems with evolutionary algorithms and proof assistants","author":"Yang L. A.","year":"2016","unstructured":"L. A. Yang , J. P. Liu , C. H. Chen , and Y. P. Chen . 2016. Automatically proving mathematical theorems with evolutionary algorithms and proof assistants . In Proceddings of CEC , 2016 . IEEE, 4421 -- 4428 . L. A. Yang, J. P. Liu, C. H. Chen, and Y. P. Chen. 2016. Automatically proving mathematical theorems with evolutionary algorithms and proof assistants. In Proceddings of CEC, 2016. IEEE, 4421--4428.","journal-title":"Proceddings of CEC"}],"event":{"name":"SAC '20: The 35th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Brno Czech Republic","acronym":"SAC '20"},"container-title":["Proceedings of the 35th Annual ACM Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341105.3373917","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341105.3373917","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:54:12Z","timestamp":1750204452000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341105.3373917"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,30]]},"references-count":21,"alternative-id":["10.1145\/3341105.3373917","10.1145\/3341105"],"URL":"https:\/\/doi.org\/10.1145\/3341105.3373917","relation":{},"subject":[],"published":{"date-parts":[[2020,3,30]]},"assertion":[{"value":"2020-03-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}