{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T01:28:53Z","timestamp":1784770133930,"version":"3.55.0"},"reference-count":56,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2023,4,1]],"date-time":"2023-04-01T00:00:00Z","timestamp":1680307200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,4,1]],"date-time":"2023-04-01T00:00:00Z","timestamp":1680307200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,4,1]],"date-time":"2023-04-01T00:00:00Z","timestamp":1680307200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"National Key Research and Development Program of China","award":["2020AAA0108800"],"award-info":[{"award-number":["2020AAA0108800"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62137002"],"award-info":[{"award-number":["62137002"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61937001"],"award-info":[{"award-number":["61937001"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62176209"],"award-info":[{"award-number":["62176209"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62176207"],"award-info":[{"award-number":["62176207"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62106190"],"award-info":[{"award-number":["62106190"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62050194"],"award-info":[{"award-number":["62050194"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61721002"],"award-info":[{"award-number":["61721002"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Innovation Research Team of Ministry of Education","award":["IRT_17R86"],"award-info":[{"award-number":["IRT_17R86"]}]},{"DOI":"10.13039\/501100002858","name":"China Postdoctoral Science Foundation","doi-asserted-by":"publisher","award":["2020M683493"],"award-info":[{"award-number":["2020M683493"]}],"id":[{"id":"10.13039\/501100002858","id-type":"DOI","asserted-by":"publisher"}]},{"name":"China Knowledge Centre for Engineering Science and Technology"},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["xzy022021048"],"award-info":[{"award-number":["xzy022021048"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["xhj032021013-02"],"award-info":[{"award-number":["xhj032021013-02"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Knowl. Data Eng."],"published-print":{"date-parts":[[2023,4,1]]},"DOI":"10.1109\/tkde.2021.3139333","type":"journal-article","created":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T20:45:52Z","timestamp":1640983552000},"page":"3563-3574","source":"Crossref","is-referenced-by-count":16,"title":["Contrastive Graph Representations for Logical Formulas Embedding"],"prefix":"10.1109","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5650-0600","authenticated-orcid":false,"given":"Qika","family":"Lin","sequence":"first","affiliation":[{"name":"School of Computer Science and Technology, Xi'an Jiaotong University, Xi'an, Shaanxi, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6004-0675","authenticated-orcid":false,"given":"Jun","family":"Liu","sequence":"additional","affiliation":[{"name":"Shaanxi Province Key Laboratory of Satellite and Terrestrial Network Tech. R&D, National Engineering Lab for Big Data Analytics, Xi'an Jiaotong University, Xi'an, Shaanxi, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8136-8795","authenticated-orcid":false,"given":"Lingling","family":"Zhang","sequence":"additional","affiliation":[{"name":"Shaanxi Province Key Laboratory of Satellite and Terrestrial Network Tech. R&D, National Engineering Lab for Big Data Analytics, Xi'an Jiaotong University, Xi'an, Shaanxi, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1942-3401","authenticated-orcid":false,"given":"Yudai","family":"Pan","sequence":"additional","affiliation":[{"name":"School of Computer Science and Technology, Xi'an Jiaotong University, Xi'an, Shaanxi, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7574-3931","authenticated-orcid":false,"given":"Xin","family":"Hu","sequence":"additional","affiliation":[{"name":"School of Computer Science and Technology, Xi'an Jiaotong University, Xi'an, Shaanxi, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fangzhi","family":"Xu","sequence":"additional","affiliation":[{"name":"School of Computer Science and Technology, Xi'an Jiaotong University, Xi'an, Shaanxi, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongwei","family":"Zeng","sequence":"additional","affiliation":[{"name":"School of Computer Science and Technology, Xi'an Jiaotong University, Xi'an, Shaanxi, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1038\/nature14539"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1038\/nature16961"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1561\/2000000039"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TNNLS.2019.2944672"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3375395.3389131"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/69.774103"},{"key":"ref7","article-title":"Neural-symbolic learning and reasoning: A survey and interpretation","author":"Besold","year":"2017","journal-title":"CoRR"},{"issue":"4","key":"ref8","first-page":"611","article-title":"Neural-symbolic computing: An effective methodology for principled integration of machine learning and reasoning","volume":"6","author":"d\u2019Avila Garcez","year":"2019","journal-title":"J. Appl. Logics"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/688"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/679"},{"key":"ref11","first-page":"4233","article-title":"Embedding symbolic knowledge into deep networks","author":"Xie","year":"2019","journal-title":"Proc. 33rd Int. Conf. Neural Inf. Process. Syst."},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA48506.2021.9561952"},{"key":"ref13","article-title":"Reasoning about entailment with neural attention","volume-title":"Proc. 4th Int. Conf. Learn. Representations","author":"Rockt\u00e4schel"},{"key":"ref14","first-page":"2235","article-title":"DeepMath - Deep sequence models for premise selection","volume-title":"Proc. 30th Int. Conf. Neural Inf. Process. Syst.","author":"Irving"},{"key":"ref15","first-page":"80","article-title":"Learning continuous semantic representations of symbolic expressions","volume-title":"Proc. 34th Int. Conf. Mach. Learn.","author":"Allamanis"},{"key":"ref16","article-title":"Can neural networks understand logical entailment?,","volume-title":"Proc. 6th Int. Conf. Learn. Representations","author":"Evans"},{"key":"ref17","first-page":"2786","article-title":"Premise selection for theorem proving by deep graph embedding","volume-title":"Proc. 31st Int. Conf. Neural Inf. Process. Syst.","author":"Wang"},{"key":"ref18","article-title":"Learning representations of logical formulae using graph neural networks","volume-title":"Proc. Neural Inf. Process. Syst., Workshop Graph Representation Learn.","author":"Glorot"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2017.243"},{"key":"ref20","article-title":"Representation learning with contrastive predictive coding","author":"Oord","year":"2018","journal-title":"CoRR"},{"key":"ref21","first-page":"1597","article-title":"A simple framework for contrastive learning of visual representations","volume-title":"Proc. 37th Int. Conf. Mach. Learn.","author":"Chen"},{"key":"ref22","article-title":"Top-down neural model for formulae","volume-title":"Proc. 7th Int. Conf. Learn. Representations","author":"Chvalovsk\u00fd"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1613\/jair.989"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i03.5689"},{"key":"ref25","article-title":"Self-supervised learning: Generative or contrastive","author":"Liu","year":"2020","journal-title":"CoRR"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/TPAMI.2020.2992393"},{"key":"ref27","article-title":"Contrastive learning of global and local features for medical image segmentation with limited annotations","volume-title":"Proc. 34th Int. Conf. Neural Inf. Process. Syst.","author":"Chaitanya"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR42600.2020.00975"},{"key":"ref29","volume-title":"A Mathematical Introduction to Logic","author":"Enderton","year":"2001"},{"key":"ref30","volume-title":"Introduction to Mathematical Logic","volume":"13","author":"Church","year":"1996"},{"key":"ref31","volume-title":"Handbook of Automated Reasoning","volume":"1","author":"Robinson","year":"2001"},{"issue":"1","key":"ref32","first-page":"101","article-title":"Hammering towards QED","volume":"9","author":"Blanchette","year":"2016","journal-title":"J. Formalized Reasoning"},{"key":"ref33","article-title":"Directed graph networks for logical reasoning","volume-title":"Proc. 7th Workshop Practical Aspects Autom. Reasoning","author":"Rawson"},{"key":"ref34","article-title":"Semi-supervised classification with graph convolutional networks","volume-title":"Proc. 5th Int. Conf. Learn. Representations","author":"Kipf"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/72.377968"},{"key":"ref36","first-page":"5998","article-title":"Attention is all you need","volume-title":"Proc. 31st Int. Conf. Neural Inf. Process. Syst.","author":"Vaswani"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2016.90"},{"key":"ref38","first-page":"448","article-title":"Batch normalization: Accelerating deep network training by reducing internal covariate shift","volume-title":"Proc. 32nd Int. Conf. Mach. Learn.","author":"Ioffe"},{"key":"ref39","first-page":"530","article-title":"Mutual information neural estimation","volume-title":"Proc. 35th Int. Conf. Mach. Learn.","author":"Belghazi"},{"key":"ref40","first-page":"271","article-title":"f-GAN: Training generative neural samplers using variational divergence minimization","volume-title":"Proc. 30th Int. Conf. Neural Inf. Process. Syst.","author":"Nowozin"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v30i1.10362"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.3115\/v1\/P15-1150"},{"key":"ref43","article-title":"Deep graph infomax","volume-title":"Proc. 7th Int. Conf. Learn. Representations","author":"Velickovic"},{"key":"ref44","article-title":"InfoGraph: Unsupervised and semi-supervised graph-level representation learning via mutual information maximization","volume-title":"Proc. 8th Int. Conf. Learn. Representations","author":"Sun"},{"key":"ref45","article-title":"Graph attention networks","volume-title":"Proc. 6th Int. Conf. Learn. Representations","author":"Velickovic"},{"key":"ref46","article-title":"Improving graph neural network representations of logical formulae with subgraph pooling","author":"Crouse","year":"2019","journal-title":"CoRR"},{"key":"ref47","first-page":"1395","article-title":"Property invariant embedding for automated reasoning","volume-title":"Proc. 24th Eur. Conf. Artif. Intell.","volume":"325","author":"Ols\u00e1k"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2019.2955502"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/3424673"},{"key":"ref50","article-title":"An empirical study of graph contrastive learning","volume-title":"Proc. Int. Conf. Neural Inf. Process. Syst.","author":"Zhu"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/3447548.3467415"},{"key":"ref52","article-title":"Adam: A method for stochastic optimization","volume-title":"Proc. 3th Int. Conf. Learn. Representations","author":"Kingma"},{"issue":"Nov","key":"ref53","first-page":"2579","article-title":"Visualizing data using t-SNE","volume":"9","author":"Maaten","year":"2008","journal-title":"J. Mach. Learn. Res."},{"key":"ref54","article-title":"Equation embeddings","author":"Krstovski","year":"2018","journal-title":"CoRR"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1145\/3341981.3344235"},{"key":"ref56","article-title":"Preliminary exploration of formula embedding for mathematical information retrieval: Can mathematical formulae be embedded like a natural language?","author":"Gao","year":"2017","journal-title":"CoRR"}],"container-title":["IEEE Transactions on Knowledge and Data Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/69\/10063074\/09667296.pdf?arnumber=9667296","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,13]],"date-time":"2024-01-13T22:08:46Z","timestamp":1705183726000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9667296\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,1]]},"references-count":56,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tkde.2021.3139333","relation":{},"ISSN":["1041-4347","1558-2191","2326-3865"],"issn-type":[{"value":"1041-4347","type":"print"},{"value":"1558-2191","type":"electronic"},{"value":"2326-3865","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,1]]}}}