×

Machine learning and logic: a new frontier in artificial intelligence. (English) Zbl 07757157

Summary: Machine learning and logical reasoning have been the two foundational pillars of Artificial Intelligence (AI) since its inception, and yet, until recently the interactions between these two fields have been relatively limited. Despite their individual success and largely independent development, there are new problems on the horizon that seem solvable only via a combination of ideas from these two fields of AI. These problems can be broadly characterized as follows: how can learning be used to make logical reasoning and synthesis/verification engines more efficient and powerful, and in the reverse direction, how can we use reasoning to improve the accuracy, generalizability, and trustworthiness of learning. In this perspective paper, we address the above-mentioned questions with an emphasis on certain paradigmatic trends at the intersection of learning and reasoning. Our intent here is not to be a comprehensive survey of all the ways in which learning and reasoning have been combined in the past. Rather we focus on certain recent paradigms where corrective feedback loops between learning and reasoning seem to play a particularly important role. Specifically, we observe the following three trends: first, the use of learning techniques (especially, reinforcement learning) in sequencing, selecting, and initializing proof rules in solvers/provers; second, combinations of inductive learning and deductive reasoning in the context of program synthesis and verification; and third, the use of solver layers in providing corrective feedback to machine learning models in order to help improve their accuracy, generalizability, and robustness with respect to partial specifications or domain knowledge. We believe that these paradigms are likely to have significant and dramatic impact on AI and its applications for a long time to come.

MSC:

68-XX Computer science
Full Text: DOI

References:

[1] Alur R, Bodik R, Juniwal G, Martin Milo MK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: Proceedings of the IEEE international conference on formal methods in computer-aided design (FMCAD), pp 1-17
[2] Abate A, David C, Kesseli P, Kroening D, Polgreen E (2018) Counterexample guided inductive synthesis modulo theories. In: Computer aided verification-30th international conference (CAV), volume 10981 of Lecture Notes in Computer Science, pp 270-288. Springer · Zbl 1511.68064
[3] Atserias, A.; Fichte, JK; Thurley, M.; Kullmann, O., Clause-learning algorithms with many restarts and bounded-width resolution, Theory and Applications of Satisfiability Testing - SAT, 114-127 (2009), Berlin, Heidelberg: Springer, Berlin Heidelberg, Berlin, Heidelberg · Zbl 1247.68245
[4] Angluin, D., Queries and concept learning, Mach Learn, 2, 4, 319-342 (1988) · Zbl 1470.68050 · doi:10.1007/BF00116828
[5] Audemard Gilles, Simon Laurent (2013) Glucose 2.3 in the SAT 2013 Competition. In: Proceedings of SAT competition 2013, pp 42-43
[6] Alur, R.; Singh, R.; Fisman, D.; Solar-Lezama, A., Search-based program synthesis, Commun ACM, 61, 12, 84-93 (2018) · doi:10.1145/3208071
[7] Ashok D, Scott J, Wetzel SJ, Panju M, Ganesh V (2021) Logic guided genetic algorithms. In: 35th AAAI conference on artificial intelligence, AAAI 2021, 33rd Conference on innovative applications of artificial intelligence, IAAI 2021, The 11th symposium on educational advances in artificial intelligence, EAAI 2021, virtual event, Feb 2-9, 2021, pp 15753-15754. AAAI Press
[8] Alaa AM, Schaar M van der (2019) Demystifying black-box models with symbolic metamodels. Adv Neural Inf Process Syst 32
[9] Bouraoui Z, Cornuéjols A, Denoeux T, Destercke S, Dubois D, Guillaume R, Marques-Silva J, Mengin J, Prade H, Schockaert S, Serrurier M, Vrain C (2019) From shallow to deep interactions between knowledge representation, reasoning and machine learning (kay r. amel group). CoRR, abs/1912.06612
[10] Biere A, Heule M, van Maaren H, Walsh T (2009) (eds) Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications. IOS Press · Zbl 1183.68568
[11] Bünz B, Lamm M (2017) Graph neural networks and boolean satisfiability. CoRR, abs/1702.03592
[12] Bengio, Y.; LeCun, Y.; Hinton, GE, Deep learning for AI, Commun ACM, 64, 7, 58-65 (2021) · doi:10.1145/3448250
[13] Bak S, Liu C, Johnson TT (2021) The second international verification of neural networks competition (VNN-COMP 2021): Summary and results. CoRR, abs/2109.00498
[14] Ball, T.; Levin, V.; Rajamani, SK, A decade of software model checking with SLAM, Commun ACM, 54, 7, 68-76 (2011) · doi:10.1145/1965724.1965743
[15] Bansal K, Loos SM, Rabe MN, Szegedy C, Wilcox S (2019) Holist: an environment for machine learning of higher order logic theorem proving. In: Kamalika C and Ruslan S, (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp 454-463. PMLR
[16] Bader-El-Den MB, Poli R (2007) Generating SAT local-search heuristics using a GP hyper-heuristic framework. In: Nicolas M, El-Ghazali T, Pierre C, Marc S, Evelyne L, (eds), Artificial Evolution, 8th International Conference, Evolution Artificielle, EA 2007, Tours, France, October 29-31, 2007, revised selected papers, volume 4926 of Lecture Notes in Computer Science, Springer, pp 37-49
[17] Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y., Bounded model checking using satisfiability solving, Formal Methods Syst Des, 19, 1, 7-34 (2001) · Zbl 0985.68038 · doi:10.1023/A:1011276507260
[18] Cropper, A.; Dumancic, S.; Evans, R.; Muggleton, SH, Inductive logic programming at 30, Mach Learn, 111, 1, 147-172 (2022) · Zbl 07510309 · doi:10.1007/s10994-021-06089-1
[19] Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs, pp 52-71 · Zbl 0546.68014
[20] Clarke EM, Fehnker A, Han Z, Krogh BH, Stursberg O, Theobald M (2003) Verification of hybrid systems based on counterexample-guided abstraction refinement. In: TACAS, pp 192-207 · Zbl 1031.68078
[21] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: 12th international conference on computer aided verification (CAV), vol. 1855 of Lecture Notes in Computer Science, Springer, pp 154-169 · Zbl 0974.68517
[22] Clarke, EM; Grumberg, O.; Jha, S.; Yuan, L.; Veith, H., Counterexample-guided abstraction refinement for symbolic model checking, J ACM, 50, 5, 752-794 (2003) · Zbl 1325.68145 · doi:10.1145/876638.876643
[23] Clarke EM, Gupta A, Kukula JH, Strichman O (2002) SAT based abstraction-refinement using ILP and machine learning techniques. In: computer aided verification, 14th international conference (CAV), vol. 2404 of Lecture Notes in Computer Science, Springer, pp 265-279 · Zbl 1010.68515
[24] Cadar C, Ganesh V, Pawlowski PM, Dill DL, Engler DR (2006) EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM conference on computer and communications security, CCS ’06, New York, NY, USA. ACM, pp 322-335
[25] Cook S (1971) The complexity of theorem-proving procedures. In: proceedings of the third annual ACM symposium on theory of computing (STOC), ACM, pp 151-158 · Zbl 0253.68020
[26] Dash T, Chitlangia S, Ahuja A, Srinivasan A (2021) How to tell deep neural networks what we know. CoRR, abs/2107.10295
[27] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Commun ACM, 5, 7, 394-397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557
[28] De Moura L, Bjørner N (2008) Z3: An efficient smt solver. In: international conference on tools and algorithms for the construction and analysis of systems, Springer, pp 337-340
[29] Duan H, Nejati S, Trimponias G, Poupart P, Ganesh V (2020) Online bayesian moment matching based SAT solver heuristics. In: Proceedings of the 37th international conference on machine learning, ICML 2020, 13-18 July 2020, Virtual Event, vol. 119 of proceedings of machine learning research, PMLR, pp 2710-2719
[30] Devlin D, O’Sullivan B (2008) Satisfiability as a classification problem. In: Proceedings of the 19th Irish Conference on artificial intelligence and cognitive science
[31] Dubois D, Prade H (2019) Towards a reconciliation between reasoning and learning-a position paper. In: Nahla Ben A, Benjamin Q, Martin T, (eds) scalable uncertainty management-13th international conference, SUM 2019, Compiègne, France, Dec 16-18, 2019, Proceedings, vol. 11940 of lecture notes in computer science, Springer, pp 153-168
[32] Eén N, Sörensson N (2004) Theory and applications of satisfiability testing: 6th international conference, SAT 2003, santa margherita ligure, Italy, May 5-8, 2003, selected revised papers, chapter an extensible SAT-solver, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 502-518 · Zbl 1204.68191
[33] Ertel W, Schumann J, Suttner CB (1989) Learning heuristics for a theorem prover using back propagation. In: Johannes R, Karl L, (eds) 5. Österreichische Artificial Intelligence-Tagung, Igls, Tirol, 28. bis 30. Sept 1989, Proceedings, vol. 208 of Informatik-Fachberichte, Springer, pp 87-95
[34] Flint A, Blaschko MB (2012) Perceptron learning of SAT. In: Bartlett PL, Pereira FNC, Burges CJC, Léon B, Weinberger KQ, (eds) Advances in neural information processing systems 25: 26th annual conference on neural information processing systems 2012. Proceedings of a meeting held Dec 3-6, 2012, Lake Tahoe, Nevada, United States, pp 2780-2788
[35] Froleyks, N.; Heule, M.; Iser, M.; Järvisalo, M.; Suda, M., SAT competition 2020, Artif Intell, 301, 103572 (2021) · Zbl 1478.68320 · doi:10.1016/j.artint.2021.103572
[36] Feldman, YMY; Immerman, N.; Sagiv, M.; Shoham, S., Complexity and information in invariant inference, Proc ACM Program Lang, 4, POPL, 5:1-5:29 (2020) · doi:10.1145/3371073
[37] First E, Rabe MN, Ringer T, Brun Y (2023) Baldur: whole-proof generation and repair with large language models. CoRR, abs/2303.04910
[38] Fukunaga AS (2002) Automated discovery of composite SAT variable-selection heuristics. In: Dechter R, Kearns MJ, Sutton RS, (eds) proceedings of the eighteenth national conference on artificial intelligence and fourteenth conference on innovative applications of artificial intelligence, July 28 - August 1, 2002, Edmonton, Alberta, Canada, AAAI Press / The MIT Press, pp 641-648
[39] Fukunaga AS (2004) Evolving local search heuristics for SAT using genetic programming. In: Kalyanmoy D, Riccardo P, Wolfgang B, Hans-Georg B, Burke EK, Darwen PJ, Dasgupta D, Floreano D, Foster JA, Mark H, Owen H, Pier Luca L, Lee S, Andrea T, Dirk T, Tyrrell AM, (eds) Genetic and evolutionary computation-GECCO 2004, genetic and evolutionary computation conference, Seattle, WA, USA, June 26-30, 2004, Proceedings, Part II, volume 3103 of Lecture Notes in Computer Science, Springer, pp 483-494
[40] Fukunaga, AS, Automated discovery of local search heuristics for satisfiability testing, Evol Comput, 16, 1, 31-61 (2008) · doi:10.1162/evco.2008.16.1.31
[41] Ian, JG; Yoshua, B.; Courville, AC, Deep Learning, Adaptive computation and machine learning (2016), Cambridge: MIT Press, Cambridge · Zbl 1373.68009
[42] Goldman, SA; Kearns, MJ, On the complexity of teaching, J Comput Syst Sci, 50, 303-314 (1992)
[43] Gupta A (2006) Learning Abstractions for Model Checking. PhD thesis, Carnegie Mellon University, June
[44] Hutter F, Babic D, Hoos HH, Hu AJ (2007) Boosting verification by automatic tuning of decision procedures. In: 7th international conference on formal methods in computer-aided design (FMCAD), IEEE Computer Society, pp 27-34
[45] Hart, PE; Nilsson, NJ; Raphael, B., A formal basis for the heuristic determination of minimum cost paths, IEEE Trans Syst Sci Cybern, 4, 2, 100-107 (1968) · doi:10.1109/TSSC.1968.300136
[46] Holden, SB, Machine learning for automated theorem proving: learning to solve SAT and QSAT, Found Trends Mach Learn, 14, 6, 807-989 (2021) · Zbl 1524.68280 · doi:10.1561/2200000081
[47] Hopfield, JJ; Tank, DW, Neural computation of decisions in optimization problems, Biol Cybern, 52, 141-152 (1985) · Zbl 0572.68041 · doi:10.1007/BF00339943
[48] Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of the 32nd international conference on software engineering (ICSE), pp 215-224
[49] Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Synthesizing switching logic for safety and dwell-time requirements. In: proceedings of the international conference on cyber-physical systems (ICCPS), pp 22-31
[50] Johnson, JL, A neural network approach to the 3-satisfiability problem, J Parallel Distributed Comput, 6, 435-449 (1989) · doi:10.1016/0743-7315(89)90068-3
[51] Jha, S.; Seshia, SA, A theory of formal synthesis via inductive learning, Acta Inform, 54, 7, 693-726 (2017) · Zbl 1380.68124 · doi:10.1007/s00236-017-0294-5
[52] Kim, S.; Lu, PY; Mukherjee, S.; Gilbert, M.; Jing, L.; Čeperić, V.; Soljačić, M., Integration of neural network-based symbolic regression in deep learning for scientific discovery, IEEE Trans Neural Netw Learn Syst, 32, 9, 4166-4177 (2021) · doi:10.1109/TNNLS.2020.3017010
[53] Kautz HA, Selman B (1992) Planning as satisfiability. In: Bernd N, (ed) 10th European conference on artificial intelligence, ECAI 92, Vienna, Austria, August 3-7, 1992. Proceedings, John Wiley and Sons, pp 359-363
[54] Kurshan R (1994) Automata-theoretic verification of coordinating processes. In: 11th international conference on analysis and optimization of systems-discrete event systems, vol. 199 of LNCS, Springer, pp 16-28
[55] Lewkowycz A, Andreassen A, Dohan D, Dyer E, Michalewski H, Ramasesh VV, Slone A, Anil C, Schlag I, Gutman-Solo T, Wu Y, Neyshabur B, Gur-Ari G, Misra V (2022) Solving quantitative reasoning problems with language models. CoRR, abs/2206.14858
[56] Liang JH, Ganesh V, Poupart P, Czarnecki K (2016) Learning rate based branching heuristic for SAT solvers. In: Nadia C, Daniel LB, (eds) Theory and applications of satisfiability testing-SAT 2016, Cham. Springer International Publishing, pp 123-140 · Zbl 1475.68348
[57] Liang JH (2018) Machine learning for SAT solvers. PhD thesis, University of Waterloo, Canada · Zbl 1511.68253
[58] Lagoudakis Michail, G.; Littman Michael, L., Learning to select branching rules in the DPLL procedure for satisfiability, Electron Notes Discrete Math, 9, 344-359 (2001) · Zbl 0990.90543 · doi:10.1016/S1571-0653(04)00332-4
[59] Liang JH, Oh C, Mathew M, Thomas C, Li C, Ganesh V (2018) Machine learning-based restart policy for CDCL SAT solvers. In: theory and applications of satisfiability testing-SAT 2018 - 21st international conference, SAT 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, pp 94-110 · Zbl 1511.68253
[60] Lederman G, Rabe MN, Seshia S, Lee EA (2020) Learning heuristics for quantified boolean formulas through reinforcement learning. In: 8th international conference on learning representations (ICLR), April
[61] Lorenz JH, Wörz F (2020) On the effect of learned clauses on stochastic local search. In: Luca P, Martina S, (eds) Theory and applications of satisfiability testing-SAT 2020-23rd international conference, Alghero, Italy, July 3-10, 2020, Proceedings, vol. 12178 of lecture notes in computer science, Springer, pp 89-106 · Zbl 07331014
[62] Tom, M., Mitchell (1997), Machine Learning: McGraw-Hill, Machine Learning · Zbl 0913.68167
[63] Marques-Silva JP, Sakallah KA (1996) GRASP-A new search algorithm for satisfiability. In: proceedings of the 1996 IEEE/ACM international conference on computer-aided design, ICCAD ’96, Washington, DC, USA. IEEE Computer Society, pp 220-227
[64] Manna, Z.; Waldinger, R., A deductive approach to program synthesis, ACM Trans Program Lang Syst (TOPLAS), 2, 1, 90-121 (1980) · Zbl 0468.68009 · doi:10.1145/357084.357090
[65] Nejati S, Frioux LL, Ganesh V (2020) A machine learning based splitting heuristic for divide-and-conquer solvers. In: Helmut S, (ed) Principles and practice of constraint programming-26th international conference, CP 2020, Louvain-la-Neuve, Belgium, Sept 7-11, 2020, Proceedings, vol. 12333 of lecture notes in computer science, Springer, pp 899-916
[66] OpenAI. GPT-4 technical report. CoRR, abs/2303.08774, 2023
[67] Panju M (2021) Automated Knowledge Discovery using Neural Networks. PhD thesis, University of Waterloo, Ontario, Canada
[68] Polgreen E, Cheang K, Gaddamadugu P, Godbole A, Laeufer K, Lin S, Manerkar YA, Mora F, Seshia SA (2022) UCLID5: multi-modal formal modeling, verification, and synthesis. In: computer aided verification-34th international conference (CAV), vol. 13371 of lecture notes in computer science, Springer, pp 538-551
[69] Pipatsrisawat, K.; Darwiche, A., On the power of clause-learning SAT solvers as resolution engines, Artif Intell, 175, 2, 512-525 (2011) · Zbl 1216.68235 · doi:10.1016/j.artint.2010.10.002
[70] Andrei, P.; Polat, ES; Alexander, F.; Mathias, U.; Müslüm, A.; Viet-Man, L.; Klaus, P.; Martin, E.; Trang, TTN, An overview of machine learning techniques in constraint solving, J Intell Inf Syst, 58, 1, 91-118 (2022) · doi:10.1007/s10844-021-00666-5
[71] Pimpalkhare N, Mora F, Polgreen E, Seshia SA (2021) MedleySolver: online SMT algorithm selection. In: 24th international conference on theory and applications of satisfiability testing (SAT), vol. 12831 of lecture notes in computer science, Springer, pp 453-470 · Zbl 07495591
[72] Pogancic MV, Paulus A, Musil V, Martius G, Rolínek M (2020) Differentiation of blackbox combinatorial solvers. In: 8th international conference on learning representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net
[73] Polgreen E, Reynolds A, Seshia SA (2022) Satisfiability and synthesis modulo oracles. In: Proceedings of the 23rd international conference on verification, model checking, and abstract interpretation (VMCAI) · Zbl 1498.68082
[74] De Raedt, L., Logical and relational learning, Cognitive technologies (2008), Berlin: Springer, Berlin · Zbl 1203.68145
[75] Russell, S.; Norvig, P., Artificial intelligence: a modern approach (2020), London: Pearson, London · Zbl 0835.68093
[76] Rossi F, van Beek P, Walsh T (2006) editors. Handbook of Constraint Programming, vol. 2 of Foundations of Artificial Intelligence. Elsevier · Zbl 1175.90011
[77] Richard, SS; Andrew, GB, Reinforcement learning-an introduction, Adaptive computation and machine learning (1998), Cambridge: MIT Press, Cambridge
[78] Seshia SA (2005) Adaptive eager boolean encoding for arithmetic reasoning in verification. PhD thesis, Carnegie Mellon University
[79] Seshia SA (2012) Sciduction: combining induction, deduction, and structure for verification and synthesis. In: proceedings of the design automation conference (DAC), pp 356-365
[80] Seshia, SA, Combining induction, deduction, and structure for verification and synthesis, Proc IEEE, 103, 11, 2036-2051 (2015) · doi:10.1109/JPROC.2015.2471838
[81] Selsam D, Lamm M, Bünz B, Liang P, de Moura L, Dill DL (2019) Learning a SAT solver from single-bit supervision. In: 7th international conference on learning representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net
[82] Solar-Lezama A, Tancau L, Bodík R, Seshia SA, Saraswat VA (2006) Combinatorial sketching for finite programs. In: proceedings of the 12th international conference on architectural support for programming languages and operating systems (ASPLOS), ACM Press, pp 404-415
[83] Scott J, Niemetz A, Preiner M, Nejati S, Ganesh V (2021) Machsmt: a machine learning-based algorithm selector for SMT solvers. In: Jan Friso G, Kim Guldstrand L, (eds) Tools and algorithms for the construction and analysis of systems-27th international conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27-April 1, 2021, Proceedings, Part II, vol. 12652 of Lecture Notes in Computer Science, Springer, pp 303-325 · Zbl 1471.68016
[84] Scott J, Panju M, Ganesh V (2020) LGML: logic guided machine learning. In: the thirty-fourth AAAI conference on artificial intelligence, AAAI 2020, the thirty-second innovative applications of artificial intelligence conference, IAAI 2020, the tenth AAAI symposium on educational advances in artificial intelligence, EAAI 2020, New York, NY, USA, Feb 7-12, 2020, AAAI Press, pp 13909-13910
[85] Marques SJP, Sakallah KA (1996) GRASP-a new search algorithm for satisfiability. In: Rutenbar RA, Otten RHJM, (eds) proceedings of the 1996 IEEE/ACM international conference on computer-aided design, ICCAD 1996, San Jose, CA, USA, Nov 10-14, 1996, IEEE Computer Society / ACM, pp 220-227
[86] Seshia SA, Subramanyan P (2018) UCLID5: integrating modeling, verification, synthesis, and learning. In: proceedings of the 15th ACM/IEEE international conference on formal methods and models for codesign (MEMOCODE)
[87] Seshia, SA; Sadigh, D.; Sastry, SS, Toward verified artificial intelligence, Commun ACM, 65, 7, 46-55 (2022) · doi:10.1145/3503914
[88] Seshia SA, Sharygina N, Tripakis S (2018) Modeling for verification. In: Clarke EM, Thomas H, Helmut V, (eds) Handbook of Model Checking, chapter 3. Springer · Zbl 1392.68264
[89] Sarker, Md; Kamruzzaman, ZL; Aaron, E.; Pascal, H., Neuro-symbolic artificial intelligence, AI Commun, 34, 3, 197-209 (2021) · Zbl 1487.68188 · doi:10.3233/AIC-210084
[90] van Harmelen F, Lifschitz V, Porter BW (2008) (eds) Handbook of Knowledge Representation, vol. 3 of Foundations of Artificial Intelligence. Elsevier · Zbl 1183.68611
[91] The Verification of Neural Networks Library (VNN-LIB). www.vnnlib.org, 2019
[92] Wang PW, Donti PL, Wilder B, Zico KJ (2019) Satnet: bridging deep learning and logical reasoning using a differentiable satisfiability solver. In: Kamalika C, Ruslan S, (eds) proceedings of the 36th international conference on machine learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, vol. 97 of Proceedings of Machine Learning Research, PMLR, pp 6545-6554
[93] Jeannette, MW, Trustworthy AI, Commun ACM, 64, 10, 64-71 (2021) · doi:10.1145/3448248
[94] Lin, X.; Hutter, F.; Hoos, HH; Leyton-Brown, K., SATzilla: portfolio-based algorithm selection for SAT, J Artif Intell Res, 32, 1, 565-606 (2008) · Zbl 1182.68272
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.