{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T22:18:13Z","timestamp":1783203493156,"version":"3.54.6"},"reference-count":65,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100019014","name":"Chengdu Science and Technology Program","doi-asserted-by":"publisher","award":["2026-RK00-00028-ZF"],"award-info":[{"award-number":["2026-RK00-00028-ZF"]}],"id":[{"id":"10.13039\/501100019014","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100012542","name":"Sichuan Provincial Science and Technology Support Program","doi-asserted-by":"publisher","award":["2024YFHZ0316"],"award-info":[{"award-number":["2024YFHZ0316"]}],"id":[{"id":"10.13039\/100012542","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004829","name":"Sichuan Province Department of Science and Technology","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004829","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002338","name":"Ministry of Education of the People's Republic of China","doi-asserted-by":"publisher","award":["20XJCZH016"],"award-info":[{"award-number":["20XJCZH016"]}],"id":[{"id":"10.13039\/501100002338","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["2682024ZTPY041"],"award-info":[{"award-number":["2682024ZTPY041"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[2026,8]]},"DOI":"10.1016\/j.artint.2026.104562","type":"journal-article","created":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T15:09:05Z","timestamp":1779289745000},"page":"104562","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["ATWGNNS: Graph simplified representation and learning of logical formula for premise selection"],"prefix":"10.1016","volume":"357","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0574-8440","authenticated-orcid":false,"given":"Xingxing","family":"He","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhongxu","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yongqi","family":"Lan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yingfang","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Li","family":"Zou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luis","family":"Mart\u00ednez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tianrui","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.artint.2026.104562_bib0001","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.jsc.2014.09.032","article-title":"Learning-assisted theorem proving with millions of lemmas","volume":"69","author":"Kaliszyk","year":"2015","journal-title":"J. Symb. Comput."},{"issue":"1\u20132","key":"10.1016\/j.artint.2026.104562_bib0002","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2003.09.001","article-title":"Introduction: progress in formal commonsense reasoning","volume":"153","author":"Davis","year":"2004","journal-title":"Artif. Intell."},{"issue":"5","key":"10.1016\/j.artint.2026.104562_bib0003","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1109\/TKDE.2009.154","article-title":"Automatic ontology matching via upper ontologies: a systematic evaluation","volume":"22","author":"Mascardi","year":"2009","journal-title":"IEEE Trans. Knowl. Data Egineering"},{"key":"10.1016\/j.artint.2026.104562_bib0004","series-title":"International Conference on Automated Deduction","first-page":"299","article-title":"Sine qua non for large theory reasoning","author":"Hoder","year":"2011"},{"key":"10.1016\/j.artint.2026.104562_bib0005","series-title":"Proceedings of the 8th International Workshop on the Implementation of Logics (IWIL-2010), Yogyakarta, Indonesia. EPiC","article-title":"Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers","volume":"2","author":"Paulson","year":"2012"},{"key":"10.1016\/j.artint.2026.104562_bib0006","series-title":"Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012)","first-page":"378","article-title":"Overview and evaluation of premise selection techniques for large theory mathematics","author":"K\u00fchlwein","year":"2012"},{"issue":"3","key":"10.1016\/j.artint.2026.104562_bib0007","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","article-title":"Mizar 40 for mizar 40","volume":"55","author":"Kaliszyk","year":"2015","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.artint.2026.104562_bib0008","series-title":"Proceedings of the International Joint Conference on Artificial Intelligence","first-page":"4877","article-title":"Graph neural networks meet neural-symbolic computing: a survey and perspective","author":"Lamb","year":"2020"},{"issue":"1","key":"10.1016\/j.artint.2026.104562_bib0009","doi-asserted-by":"crossref","first-page":"738","DOI":"10.1109\/TPAMI.2022.3140382","article-title":"Learning to guide a saturation-based theorem prover","volume":"45","author":"Abdelaziz","year":"2023","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"key":"10.1016\/j.artint.2026.104562_bib0010","series-title":"Proceedings of the Conference and Workshop on Neural Information Processing Systems (NeurIPS)","first-page":"2030","article-title":"Embedding logical queries on knowledge graphs","volume":"31","author":"Hamilton","year":"2018"},{"key":"10.1016\/j.artint.2026.104562_bib0011","series-title":"Proceedings of the 5th International Conference on Learning Representations","first-page":"1","article-title":"Semi-supervised classification with graph convolutional networks","author":"Kipf","year":"2017"},{"key":"10.1016\/j.artint.2026.104562_bib0012","unstructured":"A.S. Kucik, K. Korovin, Premise selection with neural networks and distributed representation of features, (2018). arXiv preprint arXiv: 1807.10268."},{"issue":"2","key":"10.1016\/j.artint.2026.104562_bib0013","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00881861","article-title":"Satchmore: Satchmo with relevancy","volume":"14","author":"Loveland","year":"1995","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.artint.2026.104562_bib0014","series-title":"FLAIRS Conference","first-page":"108","article-title":"Proving harder theorems by axiom reduction","author":"Sutcliffe","year":"2003"},{"key":"10.1016\/j.artint.2026.104562_bib0015","series-title":"International Conference on Automated Deduction","first-page":"295","article-title":"SRASS-a semantic relevance axiom selection system","author":"Sutcliffe","year":"2007"},{"issue":"1","key":"10.1016\/j.artint.2026.104562_bib0016","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","article-title":"Lightweight relevance filtering for machine-generated resolution problems","volume":"7","author":"Meng","year":"2009","journal-title":"J. Appl. Log."},{"issue":"2","key":"10.1016\/j.artint.2026.104562_bib0017","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","article-title":"Premise selection for mathematics by corpus analysis and kernel methods","volume":"52","author":"Alama","year":"2014","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.artint.2026.104562_bib0018","series-title":"Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (ESARLT)","first-page":"45","article-title":"MaLARea: a metasystem for automated reasoning in large theories","volume":"257","author":"Urban","year":"2007"},{"key":"10.1016\/j.artint.2026.104562_bib0019","series-title":"Third International Workshop on Proof Exchange for Theorem Proving","first-page":"87","article-title":"Stronger automation for Flyspeck by feature weighting and strategy evolution","author":"Kaliszyk","year":"2013"},{"key":"10.1016\/j.artint.2026.104562_bib0020","unstructured":"N. Kalchbrenner, E. Grefenstette, P. Blunsom, A convolutional neural network for modelling sentences, (2014). arXiv preprint arXiv: 1404.2188."},{"key":"10.1016\/j.artint.2026.104562_bib0021","series-title":"Proceedings of the Conference and Workshop on Neural Information Processing Systems (NeurIPS)","first-page":"2235","article-title":"DeepMath - deep sequence models for premise selection","volume":"29","author":"Irving","year":"2016"},{"key":"10.1016\/j.artint.2026.104562_bib0022","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods","first-page":"263","article-title":"MaLeCoP machine learning connection prover","author":"Urban","year":"2011"},{"issue":"2","key":"10.1016\/j.artint.2026.104562_bib0023","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","article-title":"Learning-assisted automated reasoning with Flyspeck","volume":"53","author":"Kaliszyk","year":"2014","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.artint.2026.104562_bib0024","unstructured":"B. Piotrowski, J. Urban, Stateful premise selection by recurrent neural networks, (2020). arXiv preprint arXiv: 2004.08212."},{"key":"10.1016\/j.artint.2026.104562_bib0025","series-title":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","first-page":"175","article-title":"Machine-learned premise selection for Lean","author":"Piotrowski","year":"2023"},{"key":"10.1016\/j.artint.2026.104562_bib0026","series-title":"Intelligent Computer Mathematics: 14th International Conference, CICM 2021, Timisoara, Romania, July 26\u201331, 2021, Proceedings 14","first-page":"84","article-title":"Improving stateful premise selection with transformers","author":"Prorokovi\u0107","year":"2021"},{"issue":"8","key":"10.1016\/j.artint.2026.104562_bib0027","doi-asserted-by":"crossref","first-page":"2057","DOI":"10.1093\/logcom\/exab006","article-title":"A study of continuous vector representations for theorem proving","volume":"31","author":"Purga\u0142","year":"2021","journal-title":"J. Log. Comput."},{"key":"10.1016\/j.artint.2026.104562_bib0028","unstructured":"I. Abdelaziz, V. Thost, M. Crouse, A. Fokoue, An experimental study of formula embeddings for automated theorem proving in first-order logic, (2020). arXiv preprint arXiv: 2002.00423."},{"key":"10.1016\/j.artint.2026.104562_bib0029","doi-asserted-by":"crossref","DOI":"10.1016\/j.jsc.2024.102376","article-title":"Graph sequence learning for premise selection","volume":"128","author":"Holden","year":"2025","journal-title":"J. Symb. Comput."},{"key":"10.1016\/j.artint.2026.104562_bib0030","series-title":"Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on the Occasion of His 60th Birthday","first-page":"54","article-title":"Learning guided automated reasoning: a brief survey","author":"Blaauwbroek","year":"2024"},{"key":"10.1016\/j.artint.2026.104562_bib0031","series-title":"Proceedings of the Conference and Workshop on Neural Information Processing Systems (NeurIPS)","first-page":"2786","article-title":"Premise selection for theorem proving by deep graph embedding","author":"Wang","year":"2017"},{"key":"10.1016\/j.artint.2026.104562_bib0032","series-title":"The Semantic Web: 15th International Conference, ESWC 2018, Heraklion, Crete, Greece, June 3\u20137, Proceedings 15","first-page":"593","article-title":"Modeling relational data with graph convolutional networks","author":"Schlichtkrull","year":"2018"},{"key":"10.1016\/j.artint.2026.104562_bib0033","unstructured":"M. Crouse, I. Abdelaziz, C. Cornelio, V. Thost, L. Wu, K. Forbus, A. Fokoue, Improving graph neural network representations of logical formulae with subgraph pooling, (2019). arXiv preprint arXiv: 1911.06904."},{"key":"10.1016\/j.artint.2026.104562_bib0034","unstructured":"M. Ol\u0161\u00e1k, C. Kaliszyk, J. Urban, Property invariant embedding for automated reasoning, (2019). arXiv preprint arXiv: 1911.12073."},{"key":"10.1016\/j.artint.2026.104562_bib0035","series-title":"Proceedings of the AAAI Conference on Artificial Intelligence","first-page":"2967","article-title":"Graph representations for higher-order logic and theorem proving","author":"Paliwal","year":"2020"},{"issue":"4","key":"10.1016\/j.artint.2026.104562_bib0036","doi-asserted-by":"crossref","first-page":"3563","DOI":"10.1109\/TKDE.2021.3139333","article-title":"Contrastive graph representations for logical formulas embedding","volume":"35","author":"Lin","year":"2021","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"10.1016\/j.artint.2026.104562_bib0037","doi-asserted-by":"crossref","DOI":"10.1016\/j.artint.2024.104209","article-title":"Approximating problems in abstract argumentation with graph convolutional networks","volume":"336","author":"Malmqvist","year":"2024","journal-title":"Artif. Intell."},{"key":"10.1016\/j.artint.2026.104562_bib0038","series-title":"Advances in Neural Information Processing Systems","first-page":"47764","article-title":"Transformers over directed acyclic graphs","volume":"36","author":"Luo","year":"2023"},{"key":"10.1016\/j.artint.2026.104562_bib0039","article-title":"Denoising heterogeneous graph pre-training framework for recommendation","author":"Sang","year":"2024","journal-title":"ACM Trans. Inf. Syst."},{"key":"10.1016\/j.artint.2026.104562_bib0040","series-title":"Proceedings of the 41st International Conference on Machine Learning","first-page":"4046","article-title":"Graph2Tac: online representation learning of formal math concepts","volume":"164","author":"Blaauwbroek","year":"2024"},{"key":"10.1016\/j.artint.2026.104562_bib0041","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"2014"},{"key":"10.1016\/j.artint.2026.104562_bib0042","series-title":"Handbook of Automated Reasoning","volume":"1","author":"Robinson","year":"2001"},{"key":"10.1016\/j.artint.2026.104562_bib0043","series-title":"First-Order Logic. Preliminaries","author":"Smullyan","year":"1968"},{"issue":"1","key":"10.1016\/j.artint.2026.104562_bib0044","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"issue":"9","key":"10.1016\/j.artint.2026.104562_bib0045","first-page":"2539","article-title":"Weisfeiler-lehman graph kernels","volume":"12","author":"Shervashidze","year":"2011","journal-title":"J. Mach. Learn. Res."},{"key":"10.1016\/j.artint.2026.104562_bib0046","series-title":"Proceedings of the International Conference on Learning Representations (ICLR 2018)","article-title":"Gamepad: a learning environment for theorem proving","author":"Huang","year":"2018"},{"key":"10.1016\/j.artint.2026.104562_bib0047","series-title":"Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-21","first-page":"85\u2014105","article-title":"Deep network guided proof search","volume":"46","author":"Sarah","year":"2017"},{"key":"10.1016\/j.artint.2026.104562_bib0048","series-title":"PAAR+ Sc2@ IJCAR","first-page":"109","article-title":"Directed graph networks for logical reasoning","author":"Rawson","year":"2020"},{"key":"10.1016\/j.artint.2026.104562_bib0049","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6\u20139, 2021, Proceedings 30","first-page":"187","article-title":"lazyCoP: lazy paramodulation meets neurally guided search","author":"Rawson","year":"2021"},{"key":"10.1016\/j.artint.2026.104562_bib0050","series-title":"Intelligent Computer Mathematics: 10th International Conference, CICM 2017","first-page":"292","article-title":"ENIGMA: efficient learning-based inference guiding machine","author":"Jakub\u016fv","year":"2017"},{"key":"10.1016\/j.artint.2026.104562_bib0051","series-title":"Proceedings of the 34th International Conference on Machine Learning (ICML)","first-page":"1263","article-title":"Neural message passing for quantum chemistry","author":"Gilmer","year":"2017"},{"issue":"4","key":"10.1016\/j.artint.2026.104562_bib0052","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","article-title":"The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0","volume":"59","author":"Sutcliffe","year":"2017","journal-title":"J. Autom. Reason."},{"issue":"1","key":"10.1016\/j.artint.2026.104562_bib0053","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1109\/TIT.1967.1053964","article-title":"Nearest neighbor pattern classification","volume":"13","author":"Cover","year":"1967","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"10.1016\/j.artint.2026.104562_bib0054","first-page":"1594","article-title":"Higher-order interaction goes neural: a substructure assembling graph attention network for graph classification","volume":"35","author":"Gao","year":"2023","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"10.1016\/j.artint.2026.104562_bib0055","series-title":"Proceedings of the Conference and Workshop on Neural Information Processing Systems (NeurIPS)","first-page":"1024","article-title":"Inductive representation learning on large graphs","volume":"30","author":"Hamilton","year":"2017"},{"key":"10.1016\/j.artint.2026.104562_bib0056","series-title":"Proceedings of the 34th International Conference on Machine Learning (ICML)","first-page":"6861","article-title":"Simplifying graph convolutional networks","author":"Wu","year":"2019"},{"key":"10.1016\/j.artint.2026.104562_bib0057","series-title":"Proceedings of the Conference and Workshop on Neural Information Processing Systems (NeurIPS)","first-page":"3844","article-title":"Convolutional neural networks on graphs with fast localized spectral filtering","volume":"29","author":"Defferrard","year":"2016"},{"key":"10.1016\/j.artint.2026.104562_bib0058","series-title":"7th International Conference on Learning Representations (ICLR 2019)","article-title":"How powerful are graph neural networks?","author":"Xu","year":"2019"},{"key":"10.1016\/j.artint.2026.104562_bib0059","unstructured":"V.P. Dwivedi, X. Bresson, A generalization of transformer networks to graphs, in: AAAI 2021 Workshop on Deep Learning on Graphs: Methods and Applications (DLG-AAAI\u201921), 2021. https:\/\/arxiv.org\/abs\/2012.09699."},{"issue":"2","key":"10.1016\/j.artint.2026.104562_bib0060","doi-asserted-by":"crossref","DOI":"10.1007\/s10489-021-02469-1","article-title":"Axiom selection over large theory based on new first-order formula metrics","volume":"52","author":"Liu","year":"2022","journal-title":"Appl. Intell."},{"key":"10.1016\/j.artint.2026.104562_bib0061","series-title":"Proceedings of the 34th International Conference on Machine Learning (ICML)","first-page":"448","article-title":"Batch normalization: accelerating deep network training by reducing internal covariate shift","author":"Ioffe","year":"2015"},{"key":"10.1016\/j.artint.2026.104562_bib0062","unstructured":"D.P. Kingma, J. Ba, Adam: A method for stochastic optimization, (2014). arXiv preprint arXiv: 1412.6980."},{"key":"10.1016\/j.artint.2026.104562_bib0063","series-title":"Proceedings of the AAAI Conference on Artificial Intelligence","article-title":"Deeper insights into graph convolutional networks for semi-supervised learning","volume":"32","author":"Li","year":"2018"},{"key":"10.1016\/j.artint.2026.104562_bib0064","series-title":"Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22","first-page":"5478","article-title":"Deep learning with logical constraints","author":"Giunchiglia","year":"2022"},{"key":"10.1016\/j.artint.2026.104562_bib0065","unstructured":"Z. Li, J. Sun, L. Murphy, Q. Su, Z. Li, X. Zhang, K. Yang, X. Si, A survey on deep learning for theorem proving, (2024). arXiv preprint arXiv: 2404.09939."}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370226000883?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370226000883?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T22:13:34Z","timestamp":1783203214000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0004370226000883"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8]]},"references-count":65,"alternative-id":["S0004370226000883"],"URL":"https:\/\/doi.org\/10.1016\/j.artint.2026.104562","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[2026,8]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"ATWGNNS: Graph simplified representation and learning of logical formula for premise selection","name":"articletitle","label":"Article Title"},{"value":"Artificial Intelligence","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.artint.2026.104562","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"104562"}}