{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T06:28:56Z","timestamp":1768112936102,"version":"3.49.0"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T00:00:00Z","timestamp":1601424000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T00:00:00Z","timestamp":1601424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100007162","name":"Guangdong Science and Technology Department","doi-asserted-by":"crossref","award":["2018B010107004"],"award-info":[{"award-number":["2018B010107004"]}],"id":[{"id":"10.13039\/501100007162","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61772038 and 61532019"],"award-info":[{"award-number":["61772038 and 61532019"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Appl Intell"],"published-print":{"date-parts":[[2021,3]]},"DOI":"10.1007\/s10489-020-01837-7","type":"journal-article","created":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T17:03:16Z","timestamp":1601485396000},"page":"1580-1601","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Proof searching and prediction in HOL4 with evolutionary\/heuristic and deep learning techniques"],"prefix":"10.1007","volume":"51","author":[{"given":"M. Saqib","family":"Nawaz","sequence":"first","affiliation":[]},{"given":"M. Zohaib","family":"Nawaz","sequence":"additional","affiliation":[]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]},{"given":"Philippe","family":"Fournier-Viger","sequence":"additional","affiliation":[]},{"given":"Meng","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,30]]},"reference":[{"key":"1837_CR1","doi-asserted-by":"crossref","unstructured":"Hasan O, Tahar S (2015) Formal verification methods. In: Encyclopedia of Information Science & Technology, 3rd edn. IGI Global, pp 7162\u20137170","DOI":"10.4018\/978-1-4666-5888-2.ch705"},{"key":"1837_CR2","unstructured":"Kaliszyk C, Chollet F, Szegedy C (2017) Holstep: A machine learning dataset for higher-order logic theorem proving. CoRR arXiv:1703.00426"},{"key":"1837_CR3","doi-asserted-by":"crossref","unstructured":"Slind K, Norrish M (2008) A brief overview of HOL4. In: Proceedings of International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pp 28\u201332","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"1837_CR4","doi-asserted-by":"crossref","unstructured":"Bertot Y, Casteran P (2004) Interactive theorem proving and program development: Coq\u2019Art: The calculus of inductive construction. Springer Publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"1837_CR5","unstructured":"Owre S, Shankar N, Rushby J M, Stringer-Calvert D W J (2001) PVS System guide, PVS prover guide PVS language reference. Technical report, SRI International"},{"key":"1837_CR6","unstructured":"Wiedijk F (Accessed on 3 January 2020) Formalizing 100 theorems, available at: http:\/\/www.cs.ru.nl\/~freek\/100"},{"key":"1837_CR7","first-page":"1","volume":"Pi 5 e2","author":"TC Hales","year":"2017","unstructured":"Hales T C, Adams M, Bauer G, Dang D T, Harrison J, Hoang T L, Kaliszyk C, Magron V, McLaughlin S, Nguyen T T, Nguyen T Q, Nipkow T, Obua S, Pleso J, Rute J M, Solovyev A, Ta A H T, Tran T N, Trieu D T, Urban J, Vu K K, Zumkeller R (2017) A formal proof of the Kepler conjecture. Forum Math Pi 5 e2:1\u201329","journal-title":"Forum Math"},{"key":"1837_CR8","doi-asserted-by":"crossref","unstructured":"Gonthier G, Asperti A, Avigad J, Bertot Y, Cohen C, Garillot F, Roux SL, Mahboubi A, O\u2019Connor R, Biha SO, Pasca I, Rideau L, Solovyev A, Tassi E, Thery L (2013) A machine-checked proof of the Odd Order theorem. In: Proceedings of International Conference on Interactive Theorem Proving (ITP), pp 163\u2013179","DOI":"10.1007\/978-3-642-39634-2_14"},{"issue":"7","key":"1837_CR9","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7):107\u2013115","journal-title":"Commun ACM"},{"key":"1837_CR10","doi-asserted-by":"crossref","unstructured":"Blanchette JC, Haslbeck MPL, Matichuk D, Nipkow T (2015) Mining the archive of formal proofs. In: Proceedings of International Conference on Intelligent Computer Mathematics (CICM), pp 3\u201317","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"1837_CR11","doi-asserted-by":"crossref","unstructured":"Harrison J, Urban J, Wiedijk F (2014) History of interactive theorem proving. In: Computational Logic, volume 9 of Handbook of the History of Logic, pp 135\u2013214","DOI":"10.1016\/B978-0-444-51624-4.50004-6"},{"key":"1837_CR12","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jsc.2014.09.032","volume":"69","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk C, Urban J (2015) Learning-assisted theorem proving with millions of lemmas. J Symb Comput 69:109\u2013128","journal-title":"J Symb Comput"},{"key":"1837_CR13","doi-asserted-by":"crossref","unstructured":"F\u00e4rber M, Brown CE (2016) Internal guidance for Satallax. In: Proceedings of International Joint Conference on Automated Reasoning (IJCAR), pp 349\u2013361","DOI":"10.1007\/978-3-319-40229-1_24"},{"key":"1837_CR14","unstructured":"Gauthier T, Kaliszyk C, Urban J (2017) TacticToe: Learning to reason with HOL4 tactics. In: Proceedings of International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pp 125\u2013143"},{"key":"1837_CR15","unstructured":"Irving G, Szegedy C, Alemi AA, E\u00e9n N, Chollet F, Urban J (2016) Deepmath - Deep sequence models for premise selection. In: Proceedings of Annual Conference on Neural Information Processing Systems (NIPS), pp 2235\u20132243"},{"key":"1837_CR16","unstructured":"Kaliszyk C, Mamane L, Urban J (2014) Machine learning of Coq proof guidance: First experiments. In: Proceedings of International Symposium on Symbolic Computation in Software Science (SCSS), pp 27\u201334"},{"key":"1837_CR17","doi-asserted-by":"crossref","unstructured":"Nawaz MS, Sun M, Fournier-Viger P (2019) Proof guidance in PVS with sequential pattern mining. In: Proceedings of International Conference on Fundamentals of Software Engineering (FSEN), pp 45\u201360","DOI":"10.1007\/978-3-030-31517-7_4"},{"key":"1837_CR18","doi-asserted-by":"crossref","unstructured":"Nawaz MZ, Hasan O, Nawaz MS, Fournier-Viger P, Sun M (2020) Proof searching in HOL4 with genetic algorithm. In: Proceedings of Annual ACM Symposium on Applied Computing (SAC), pp 513\u2013520","DOI":"10.1145\/3341105.3373917"},{"key":"1837_CR19","unstructured":"Huang SY, Chen YP (2017) Proving theorems by using evolutionary search with human involvement. In: Proceedings of Congress on Evolutionary Computation (CEC), pp 1495\u20131502"},{"key":"1837_CR20","doi-asserted-by":"crossref","unstructured":"Yang LA, Liu JP, Chen CH, Chen YP (2016) Automatically proving mathematical theorems with evolutionary algorithms and proof assistants. In: Proceedings of Congress on Evolutionary Computation (CEC), pp 4421\u20134428","DOI":"10.1109\/CEC.2016.7744352"},{"key":"1837_CR21","volume-title":"Genetic programming - On the programming of computers by means of natural selection","author":"JR Koza","year":"1993","unstructured":"Koza J R (1993) Genetic programming - On the programming of computers by means of natural selection. MIT Press Cambridge, Massachusetts"},{"key":"1837_CR22","unstructured":"Duncan H (2007) The use of data-mining for the automatic formation of tactics. PhD Thesis, University of Edinburgh, UK"},{"issue":"2","key":"1837_CR23","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2014","unstructured":"Alama J, Heskes T, Ku\u0307hlwein D, Tsivtsivadze E, Urban J (2014) Premise selection for mathematics by corpus analysis and kernel methods. J Auto Reaso 52(2):191\u2013213","journal-title":"J Auto Reaso"},{"key":"1837_CR24","unstructured":"Loos SM, Irving G, Szegedy C, Kaliszyk C (2017) Deep network guided proof search. In: Proceedings of International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pp 85\u2013105"},{"key":"1837_CR25","unstructured":"Wang M, Tang Y, Wang J, Deng J (2017) Premise selection for theorem proving by deep graph embedding. In: Proceedings of Annual Conference on Neural Information Processing Systems (NIPS), pp 2786\u20132796"},{"key":"1837_CR26","unstructured":"Whalen D (2016) Holophrasm: a neural automated theorem prover for higher-order logic. CoRR arXiv:1608.02644"},{"key":"1837_CR27","doi-asserted-by":"crossref","unstructured":"Gauthier T, Kaliszyk C (2015) Premise selection and external provers for HOL4. In: Proceedings of International Conference on Certified Programs and Proofs (CPP), pp 49\u201357","DOI":"10.1145\/2676724.2693173"},{"issue":"1","key":"1837_CR28","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk C, Urban J (2015) Hol(y)hammer: Online ATP service for HOL light. Mathe Comp Sci 9(1):5\u201322","journal-title":"Mathe Comp Sci"},{"key":"1837_CR29","doi-asserted-by":"crossref","unstructured":"Zhang X, Li Y, Hong W, Sun M (2019) Using recurrent neural network to predict tactics for proving component connector properties in Coq. In: Proceedings of International Symposium on Theoretical Aspects of Software Engineering (TASE), pp 107\u2013112","DOI":"10.1109\/TASE.2019.00-12"},{"key":"1837_CR30","unstructured":"Holland J H (1975) Adaptation in natural and artificial systems. University of Michigan Press, Ann Arbor"},{"key":"1837_CR31","doi-asserted-by":"crossref","unstructured":"Mitchell M (1996) An introduction to genetic algorithms. MIT Press Cambridge, Massachusetts","DOI":"10.7551\/mitpress\/3927.001.0001"},{"issue":"1","key":"1837_CR32","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1012815625611","volume":"16","author":"T Hong","year":"2002","unstructured":"Hong T, Wang H, Lin W, Lee W Y (2002) Evolution of appropriate crossover and mutation operators in a genetic process. Appl Intell 16(1):7\u201317","journal-title":"Appl Intell"},{"issue":"1","key":"1837_CR33","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1214\/ss\/1177011077","volume":"8","author":"D Bertsimas","year":"2013","unstructured":"Bertsimas D, Tsitsiklis J (2013) Simulated annealing. Stati Sci 8(1):10\u201315","journal-title":"Stati Sci"},{"key":"1837_CR34","doi-asserted-by":"crossref","unstructured":"Delahaye D, Chaimatanan S, Mongeau M (2019) Simulated annealing: From basics to applications. In: Handbook of Metaheuristics, pp 1\u201335","DOI":"10.1007\/978-3-319-91086-4_1"},{"issue":"3","key":"1837_CR35","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1023\/A:1011288128914","volume":"15","author":"X Yao","year":"2001","unstructured":"Yao X, McKay R I (2001) Simulated evolution and learning: an introduction. Appl Intell 15 (3):151\u2013152","journal-title":"Appl Intell"},{"key":"1837_CR36","doi-asserted-by":"crossref","unstructured":"Graves A (2012) Supervised sequence labelling with recurrent neural networks. Springer Publisher","DOI":"10.1007\/978-3-642-24797-2"},{"key":"1837_CR37","doi-asserted-by":"crossref","unstructured":"Medsker L, Jain LC (1999) Recurrent neural networks: Design and applications. CRC Press","DOI":"10.1201\/9781420049176"},{"issue":"8","key":"1837_CR38","doi-asserted-by":"publisher","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","volume":"9","author":"S Hochreiter","year":"1997","unstructured":"Hochreiter S, Schmidhuber J (1997) Long short-term memory. Neur Comp 9(8):1735\u20131780","journal-title":"Neur Comp"},{"issue":"1","key":"1837_CR39","first-page":"54","volume":"1","author":"P Fournier-Viger","year":"2017","unstructured":"Fournier-Viger P, Lin J C W, Kiran R U, Koh Y S, Thomas R (2017) A survey of sequential pattern mining. Data Sci Patt Recogn 1(1):54\u201377","journal-title":"Data Sci Patt Recogn"},{"key":"1837_CR40","unstructured":"Python codes and HOL4 data, available at: github.com\/MuhammadzohaibNawaz\/PRS-GA-and-SA-in-Python"},{"issue":"2","key":"1837_CR41","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1016\/j.ejor.2006.02.012","volume":"178","author":"AL Nsakanda","year":"2007","unstructured":"Nsakanda A L, Price W L, Diaby M, Gravel M (2007) Ensuring population diversity in genetic algorithms: a technical note with application to the cell formation problem. Euro J Operat Rese 178 (2):634\u2013638","journal-title":"Euro J Operat Rese"},{"issue":"7587","key":"1837_CR42","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver D, Huang A, Maddison C J, Guez A, Sifre L, van den Driessche G, Schrittwieser J, Antonoglou I, Panneershelvam V, Lanctot M, Dieleman S, Grewe D, Nham J, Kalchbrenner N, Sutskever I, Lillicrap T P, Leach M, Kavukcuoglu K, Graepel T, Hassabis D (2016) Mastering the game of Go with deep neural networks and tree search. Nature 529(7587):484\u2013489","journal-title":"Nature"},{"key":"1837_CR43","unstructured":"Kaiser L, Sutskever I (2016) Neural GPUs learn algorithms In: International Conference on Learning Representations, (ICLR). Poster"},{"key":"1837_CR44","unstructured":"Sukhbaatar S, Szlam A, Weston J, Fergus R (2015) End-to-end memory networks. In: Proceedings of Annual Conference on Neural Information Processing Systems (NIPS). pp 2440\u20132448"},{"key":"1837_CR45","unstructured":"Wu Y, Schuster M, Chen Z, Le Q V, Norouzi M, Macherey M, Krikun M, Cao Y, Gao Q, Macherey Q, Klingner J, Shah A, Johnson M, Liu X, Kaiser L, Gouws S, Kato Y, Kudo T, Kazawa H, Stevens K, Kurian G, Patil N, Wang W, Young C, Smith J, Riesa J, Rudnick A, Vinyals O, Corrado G, Hughes M, Dean J (2016) Google\u2019s neural machine translation system: Bridging the gap between human and machine translation. CoRR arXiv:1609.08144"},{"key":"1837_CR46","unstructured":"Vinyals Q, Le Q V (2015) A neural conversational model. CoRR arXiv:1506.05869"},{"key":"1837_CR47","unstructured":"Socher R, Chen D, Manning CD, Ng AY (2013) Reasoning with neural tensor networks for knowledge base completion. In: Proceedings of Annual Conference on Neural Information Processing Systems (NIPS), pp 926\u2013934"},{"key":"1837_CR48","unstructured":"Nawaz M S, Malik M, Li Y, Sun M, Lali M I (2019) A survey on theorem provers in formal methods. CoRR arXiv:1912.03028"},{"issue":"3","key":"1837_CR49","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"GP Huet","year":"1973","unstructured":"Huet G P (1973) The undecidability of unification in third order logic. Informa Cont 22 (3):257\u2013267","journal-title":"Informa Cont"},{"issue":"2","key":"1837_CR50","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1142\/S0218488598000094","volume":"6","author":"S Hochreiter","year":"1998","unstructured":"Hochreiter S (1998) The vanishing gradient problem during learning recurrent neural nets and problem solutions. Int J Uncertain Fuzz 6(2):107\u2013116","journal-title":"Int J Uncertain Fuzz"},{"key":"1837_CR51","unstructured":"Olah C (2015) Understanding LSTM networks, available at: https:\/\/colah.github.io\/posts\/2015-08-Understanding-LSTMs"},{"key":"1837_CR52","unstructured":"Abadi M, Barham P, Chen J, Chen Z, Davis A, Dean J, Devin M, Ghemawat S, Irving G, Isard M, Kudlur M, Levenberg J, Monga R, Moore S, Murray DG, Steiner B, Tucker PA, Vasudevan V, Warden P, Wicke M, Yu Y, Zheng X (2016) Tensorflow: A system for large-scale machine learning. In: Proceedings of USENIX Symposium on Operating Systems Design and Implementation (OSDI), pp 265\u2013283"},{"key":"1837_CR53","unstructured":"Jones T (1995) Crossover, macromutationand, and population-based search. In: Proceedings of the 6th International Conference on Genetic Algorithms (ICGA), pp 73\u201380"},{"key":"1837_CR54","doi-asserted-by":"crossref","unstructured":"Kennedy J, Eberhart R (1995) Particle swarm optimization. In: Proceedings of International Conference on Neural Networks (ICNN), pp 1942\u20131948","DOI":"10.1109\/ICNN.1995.488968"},{"issue":"1","key":"1837_CR55","first-page":"1","volume":"4","author":"CB Browne","year":"2012","unstructured":"Browne C B, Powley E, Whitehouse D, Lucas S M, Cowling I, Rohlfshagen P, Tavener S, Perez D, Samothrakis S, Colton S (2012) A survey of monte carlo tree search methods. IEEE Trans Comp Intell AI 4(1):1\u201343","journal-title":"IEEE Trans Comp Intell AI"},{"issue":"1","key":"1837_CR56","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/s10489-009-0179-6","volume":"34","author":"B Shuan","year":"2011","unstructured":"Shuan B, Chen J, Li Z (2011) Study on hybrid PS-ACO algorithm. Appl Intell 34(1):64\u201373","journal-title":"Appl Intell"},{"key":"1837_CR57","unstructured":"Santo JE (2015) Curry-howard for sequent calculus at last! In: Proceedings of International Conference on Typed Lambda Calculi and Applications (TLCA), pp 165\u2013179"},{"key":"1837_CR58","doi-asserted-by":"crossref","unstructured":"Cho K, van Merrienboer B, Bahdanau D, Bengio Y (2014) On the properties of neural machine translation: Encoder-decoder approaches. In: Proceedings of Workshop on Syntax, Semantics and Structure in Statistical Translation (SSST@EMNLP), pp 103\u2013111","DOI":"10.3115\/v1\/W14-4012"}],"container-title":["Applied Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10489-020-01837-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10489-020-01837-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10489-020-01837-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T05:59:24Z","timestamp":1723701564000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10489-020-01837-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,30]]},"references-count":58,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,3]]}},"alternative-id":["1837"],"URL":"https:\/\/doi.org\/10.1007\/s10489-020-01837-7","relation":{},"ISSN":["0924-669X","1573-7497"],"issn-type":[{"value":"0924-669X","type":"print"},{"value":"1573-7497","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9,30]]},"assertion":[{"value":"30 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Compliance with Ethical Standards"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of interests"}}]}}