×

zbMATH — the first resource for mathematics

Machine learning guidance for connection tableaux. (English) Zbl 07356974
Summary: Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: first, we show optimised functional implementations of connection tableaux proof search, including a consistent Skolemisation procedure for machine learning. Then, we show two guidance methods based on machine learning, namely reordering of proof steps with Naive Bayesian probabilities, and expansion of a proof search tree with Monte Carlo Tree Search.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alama, J., Kühlwein, D., Urban, J.: Automated and human proofs in general mathematics: an initial comparison. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18, vol. 7180 of LNCS, 37-45. Springer (2012). doi:10.1007/978-3-642-28717-6_6. ISBN 978-3-642-28716-9 · Zbl 1352.68211
[2] Alama, J.; Heskes, T.; Kühlwein, D.; Tsivtsivadze, E.; Urban, J., Premise selection for mathematics by corpus analysis and kernel methods, J. Autom. Reason., 52, 2, 191-213 (2014) · Zbl 1315.68217
[3] Andrews, PB, On connections and higher-order logic, J. Autom. Reason., 5, 3, 257-291 (1989) · Zbl 0694.03011
[4] Armando, A., Baumgartner, P., Dowek, G. (eds.): IJCAR, vol. 5195 of LNCS. Springer (2008).doi:10.1007/978-3-540-71070-7. ISBN 978-3-540-71069-1 · Zbl 1149.68003
[5] Beckert, B.; Posegga, J., leanTAP: lean tableau-based deduction, J. Autom. Reason., 15, 3, 339-358 (1995) · Zbl 0838.68097
[6] Beckert, Bernhard, Hähnle, Reiner, Schmitt, Peter H.: The even more liberalized \(\delta \)-rule in free variable semantic tableaux. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) Kurt gödel colloquium, vol. 713 of LNCS, pp. 108-119. Springer (1993). doi:10.1007/BFb0022559. ISBN 3-540-57184-1 · Zbl 0794.03020
[7] Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.): TPHOLs, vol. 5674 of LNCS. Springer (2009). doi:10.1007/978-3-642-03359-9. ISBN 978-3-642-03358-2 · Zbl 1173.68002
[8] Bertot, Y.: A short presentation of Coq. In: Mohamed, O.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs, vol. 5170 of LNCS, pp. 12-16. Springer (2008). doi:10.1007/978-3-540-71067-7_3. ISBN 978-3-540-71065-3 · Zbl 1165.68449
[9] Bibel, W., Matings in matrices, Commun. ACM, 26, 11, 844-852 (1983) · Zbl 0519.68078
[10] Bibel, W.: Automated Theorem Proving, 2nd edn. Artificial Intelligence. Vieweg (1987). http://www.worldcat.org/oclc/16641802 · Zbl 0639.68092
[11] Bibel, W.: Perspectives on automated deduction. In: Boyer, R.S. (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe. Automated Reasoning Series, pp. 77-104. Kluwer Academic Publishers (1991). ISBN 0-7923-1409-3
[12] Bibel, W.: A vision for automated deduction rooted in the connection method. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX, vol. 10501 of LNCS, pp. 3-21. Springer (2017). doi:10.1007/978-3-319-66902-1_1. ISBN 978-3-319-66901-4 · Zbl 06833546
[13] Biere, A., Dragan, I., Kovács, L., Voronkov, A.: Experimenting with SAT solvers in Vampire. In: Gelbukh, A.F., Castro, F., Espinoza, Q., Galicia, S.N., Haro, Q. (eds.) MICAI 2014. part I, vol. 8856 of LNCS, pp. 431-442. Springer (2014). doi:10.1007/978-3-319-13647-9_39. ISBN 978-3-319-13646-2
[14] Blanchette, JC; Kaliszyk, C.; Paulson, LC; Urban, J., Hammering towards QED, J. Formaliz. Reason., 9, 1, 101-148 (2016) · Zbl 1451.68318
[15] Blanchette, JC; Greenaway, D.; Kaliszyk, C.; Kühlwein, D.; Urban, J., A learning-based fact selector for Isabelle/HOL, J. Autom. Reason., 57, 3, 219-244 (2016) · Zbl 1386.68149
[16] Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda—a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs, vol. 5674 of LNCS, pp. 73-78. Springer (2009). doi:10.1007/978-3-642-03359-9_6. ISBN 978-3-642-03358-2 · Zbl 1252.68062
[17] Browne, C.; Powley, EJ; Whitehouse, D.; Lucas, SM; Cowling, PI; Rohlfshagen, P.; Tavener, S.; Liebana, DP; Samothrakis, S.; Colton, S., A survey of Monte Carlo tree search methods, IEEE Trans. Comput. Intell. AI Games, 4, 1, 1-43 (2012)
[18] Brünnler, K., Metcalfe, G. (eds.). TABLEAUX, vol. 6793 of LNCS. Springer (2011). doi:10.1007/978-3-642-22119-4. ISBN 978-3-642-22118-7 · Zbl 1216.68022
[19] Carlson, A.J., Cumby, C.M., Rosen, J.L., Roth, D.: SNoW user guide, Technical Report UIUCDCS-R-99-2101, University of Illinois at Urbana-Champaign (1999). http://cogcomp.org/papers/CCRR99.pdf
[20] Denzinger, J., Fuchs, M., Goller, C., Schulz, S.: Learning from Previous Proof Experience, Technical Report AR99-4, Institut für Informatik, Technische Universität München (1999)
[21] Färber, M., Brown, C.E.: Internal guidance for Satallax. In: Olivetti, N., Tiwari, A. (eds.) IJCAR, vol. 9706 of LNCS, pp. 349-361. Springer (2016). doi:10.1007/978-3-319-40229-1_24. ISBN 978-3-319-40228-4 · Zbl 06623272
[22] Färber, M., Kaliszyk, C., Urban, J.: Monte Carlo tableau proof search. In: de Moura, L. (ed.) CADE-26, vol. 10395 of LNCS, pp. 563-579. Springer (2017). doi:10.1007/978-3-319-63046-5_34. ISBN 978-3-319-63045-8 · Zbl 06778426
[23] Galmiche, D., Connection methods in linear logic and proof nets construction, Theor. Comput. Sci., 232, 1-2, 231-272 (2000) · Zbl 0951.03055
[24] Giese, M., Ahrendt, W.: Hilbert’s epsilon-terms in automated theorem proving. In: Murray, N.V. (ed.)TABLEAUX, vol. 1617 of LNCS, pp. 171-185. Springer (1999). doi:10.1007/3-540-48754-9_17. ISBN 3-540-66086-0 · Zbl 0931.03016
[25] Greenbaum, S.: Input transformations and resolution implementation techniques for theorem-proving in first-order logic. Ph.D. diss, University of Illinois at Urbana-Champaign (1986)
[26] Hähnle, R.: Tableaux and related methods. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 100-178. Elsevier, MIT Press (2001). ISBN 0-444-50813-9 · Zbl 1011.68125
[27] 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., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. Forum of Mathematics, Pi 5. (2017). doi:10.1017/fmp.2017.1 · Zbl 1379.52018
[28] Harrison, J.: HOL Light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs, vol. 5674 of LNCS, pp. 60-66. Springer (2009). doi:10.1007/978-3-642-03359-9_4. ISBN 978-3-642-03358-2
[29] Hilbert, D., Bernays, P.: Grundlagen der Mathematik. II, vol. 50 of Die Grundlehren der mathematischen Wissenschaften. Springer (1939) · Zbl 0020.19301
[30] Hintikka, J., Game-theoretical semantics: insights and prospects, Notre Dame J. Form. Log., 23, 2, 219-241 (1982) · Zbl 0464.03008
[31] Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjørner, N., Stokkermans, V.S. (eds.) CADE-23, vol. 6803 of LNCS, pp. 299-314. Springer (2011). doi:10.1007/978-3-642-22438-6_23. ISBN 978-3-642-22437-9 · Zbl 1341.68189
[32] Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR, vol. 9706 of LNCS, pp. 313-329. Springer (2016). doi:10.1007/978-3-319-40229-1_22. ISBN 978-3-319-40228-4 · Zbl 06623270
[33] Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Muñoz, C. (eds.) Design and application of strategies/tactics in higher order logics (STRATA). NASA technical reports, pp. 56-68 (2003). http://www.gilith.com/research/papers
[34] Irving, G., Szegedy, C., Alemi, A.A., Eén, N., Chollet, F., Urban, J.: DeepMath—deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) NIPS, pp. 2235-2243 (2016). http://papers.nips.cc/paper/6280-deepmath-deep-sequence-models-for-premise-selection
[35] Jakub \(\mathring{{\rm u}}\) v, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM, vol. 10383 of LNCS, pp. 292-302. Springer (2017). doi:10.1007/978-3-319-62075-6_20. ISBN 978-3-319-62074-9
[36] Jones, KS, Index term weighting, Inf. Storage Retr., 9, 11, 619-633 (1973)
[37] Kaliszyk, C.; Urban, J., Learning-assisted automated reasoning with Flyspeck, J. Autom. Reason., 53, 2, 173-213 (2014) · Zbl 1314.68283
[38] Kaliszyk, C., Urban, J.: FEMaLeCoP: Fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20, vol. 9450 of LNCS, pp. 88-96. Springer (2015). doi:10.1007/978-3-662-48899-7_7. ISBN 978-3-662-48898-0 · Zbl 06528775
[39] Kaliszyk, C.; Urban, J., HOL(y)Hammer: online ATP service for HOL light, Math. Comput. Sci., 9, 1, 5-22 (2015) · Zbl 1322.68177
[40] Kaliszyk, C.; Urban, J., MizAR 40 for Mizar 40, J. Autom. Reason., 55, 3, 245-256 (2015) · Zbl 1356.68191
[41] Kaliszyk, C., Urban, J., Vyskočil, J.: Certified connection tableaux proofs for HOL Light and TPTP. In: Leroy, X., Tiu, A. (eds.) CPP, pp. 59-66. ACM (2015). doi:10.1145/2676724.2693176. ISBN 978-1-4503-3296-5
[42] Kaliszyk, C., Urban, J., Vyskočil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) IJCAI, pp. 3084-3090. AAAI Press (2015). ISBN 978-1-57735-738-4. http://ijcai.org/Abstract/15/435
[43] Kaliszyk, C., Schulz, S., Urban, J., Vyskočil, J.: System description: E.T. 0.1. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25, vol. 9195 of LNCS, pp. 389-398. Springer (2015). doi:10.1007/978-3-319-21401-6_27. ISBN 978-3-319-21400-9 · Zbl 1465.68286
[44] Kocsis, L., Szepesvári, C.: Bandit based Monte-Carlo planning. In: Fürnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) ECML, vol. 4212 of LNCS, pp. 282-293. Springer (2006). doi:10.1007/11871842_29. ISBN 3-540-45375-X
[45] Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV, vol. 8044 of LNCS, pp. 1-35. Springer (2013). doi:10.1007/978-3-642-39799-8_1. ISBN 978-3-642-39798-1
[46] Kühlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR, vol. 7364 of LNCS, pp. 378-392. Springer (2012). doi:10.1007/978-3-642-31365-3_30. ISBN 978-3-642-31364-6 · Zbl 1358.68259
[47] Kühlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP, vol. 7998 of LNCS, pp. 35-50. Springer (2013). doi:10.1007/978-3-642-39634-2_6 · Zbl 1317.68215
[48] Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 2015-2114. Elsevier, MIT Press (2001). ISBN 0-444-50813-9 · Zbl 1011.68130
[49] Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W., SETHEO: a high-performance theorem prover, J. Autom. Reason., 8, 2, 183-212 (1992) · Zbl 0759.68080
[50] Loos, S.M., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: Eiter, T., Sands, D. (eds.) LPAR-21, vol. 46 of Epic series in computing, pp. 85-105. EasyChair (2017). http://www.easychair.org/publications/paper/340345 · Zbl 1403.68197
[51] Loveland, DW, Mechanical theorem-proving by model elimination, J. ACM, 15, 2, 236-251 (1968) · Zbl 0162.02804
[52] Meng, J.; Paulson, LC, Lightweight relevance filtering for machine-generated resolution problems, J. Appl. Log., 7, 1, 41-57 (2009) · Zbl 1183.68560
[53] Mohamed, O.A., Muñoz, C.A., Tahar, S. (eds.). TPHOLs, vol. 5170 of LNCS. Springer (2008). doi:10.1007/978-3-540-71067-7. ISBN 978-3-540-71065-3
[54] Nonnengart, A.: Strong skolemization, Research Report MPI-I-96-2-010, Max-Planck-Institut für Informatik, Im Stadtwald, Saarbrücken, Germany (1996)
[55] Olivetti, N., Tiwari, A. (eds.): IJCAR. Vol. 9706 of LNCS. Springer (2016). doi:10.1007/978-3-319-40229-1. ISBN 978-3-319-40228-4
[56] Otten, J.: Clausal connection-based theorem proving in intuitionistic first-order logic. In: Beckert, B. (ed.) TABLEAUX, vol. 3702 of LNCS, pp. 245-261. Springer (2005). doi:10.1007/11554554_19. ISBN 3-540-28931-3 · Zbl 1142.03331
[57] Otten, J.: leanCoP 2.0 and ileanCoP 1.2: high performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR, vol. 5195 of LNCS, pp. 283-291. Springer (2008). doi:10.1007/978-3-540-71070-7_23. ISBN 978-3-540-71069-1 · Zbl 1165.68467
[58] Otten, J., Restricting backtracking in connection calculi, AI Commun., 23, 2-3, 159-182 (2010) · Zbl 1205.68363
[59] Otten, J.: A non-clausal connection calculus. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX, vol. 6793 of LNCS, pp. 226-241. Springer (2011). doi:10.1007/978-3-642-22119-4_18. ISBN 978-3-642-22118-7 · Zbl 1333.03004
[60] Otten, J.: Mleancop: a connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR, vol. 8562 of LNCS, pp. 269-276. Springer (2014). doi:10.1007/978-3-319-08587-6_20. ISBN 978-3-319-08586-9 · Zbl 1423.68423
[61] Otten, J.: nanoCoP: a non-clausal connection prover. In: Olivetti, N., Tiwari, A. (eds.) IJCAR, vol. 9706 of LNCS, pp. 302-312. Springer (2016). doi:10.1007/978-3-319-40229-1_21. ISBN 978-3-319-40228-4 · Zbl 06623269
[62] Otten, J.; Bibel, W., leanCoP: lean connection-based theorem proving, J. Symb. Comput., 36, 1-2, 139-161 (2003) · Zbl 1025.68076
[63] Plaisted, DA; Greenbaum, S., A structure-preserving clause form translation, J. Symb. Comput., 2, 3, 293-304 (1986) · Zbl 0636.68119
[64] Plotkin, GD, Call-by-name, call-by-value and the lambda-calculus, Theor. Comput. Sci., 1, 2, 125-159 (1975) · Zbl 0325.68006
[65] Ramakrishnan, I.V., Sekar, R.C., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1853-1964. Elsevier, MIT Press (2001). ISBN 0-444-50813-9 · Zbl 0992.68189
[66] Raths, T., Otten, J.: randoCoP: randomizing the proof search order in the connection calculus. In: Konev, B., Schmidt, R.A., Schulz, S. (eds.) PAAR, vol. 373 of CEUR Workshop Proceedings. CEUR-WS.org (2008). http://ceur-ws.org/Vol-373/paper-08.pdf
[67] Raths, T.; Otten, J.; Kreitz, C., The ILTP problem library for intuitionistic logic, J. Autom. Reason., 38, 1-3, 261-271 (2007) · Zbl 1113.68093
[68] Robinson, JA; Voronkov, A., Handbook of Automated Reasoning (in 2 volumes) (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0964.00020
[69] Rosin, C.D.: Nested rollout policy adaptation for Monte Carlo tree search. In: Walsh, T. (ed.) IJCAI, pp. 649-654. IJCAI/AAAI (2011). doi:10.5591/978-1-57735-516-8/IJCAI11-115. ISBN 978-1-57735-516-8
[70] Schadd, MPD; Winands, MHM; Tak, MJW; Uiterwijk, JWHM, Single-player Monte-Carlo tree search for samegame, Knowl. Based Syst., 34, 3-11 (2012)
[71] Schulz, S.: Learning search control knowledge for equational theorem proving. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI, vol. 2174 of LNCS, pp. 320-334. Springer (2001). doi:10.1007/3-540-45422-5_23. ISBN 3-540-42612-4 · Zbl 1007.68576
[72] Schulz, S.: System description: E 1.8. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) LPAR-19, vol. 8312 of LNCS, pp. 735-743. Springer (2013). doi:10.1007/978-3-642-45221-5_49. ISBN 978-3-642-45220-8 · Zbl 1407.68442
[73] Silver, D.; Huang, A.; Maddison, CJ; 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, TP; Leach, M.; Kavukcuoglu, K.; Graepel, T.; Hassabis, D., Mastering the game of Go with deep neural networks and tree search, Nature, 529, 7587, 484-489 (2016)
[74] Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs, vol. 5170 of LNCS, pp. 28-32. Springer (2008). doi:10.1007/978-3-540-71067-7_6. ISBN 978-3-540-71065-3 · Zbl 1165.68474
[75] Sutcliffe, G., The 4th IJCAR automated theorem proving system competition—CASC-J4, AI Commun., 22, 1, 59-72 (2009)
[76] Sutcliffe, G., The TPTP problem library and associated infrastructure, J. Autom. Reason., 43, 4, 337-362 (2009) · Zbl 1185.68636
[77] Sutcliffe, G., The 5th IJCAR automated theorem proving system competition—CASC-J5, AI Commun., 24, 1, 75-89 (2011)
[78] Sutcliffe, G., The 8th IJCAR automated theorem proving system competition—CASC-J8, AI Commun., 29, 5, 607-619 (2016) · Zbl 1373.68367
[79] Sutcliffe, G., The CADE ATP system competition—CASC, AI Mag., 37, 2, 99-101 (2016) · Zbl 0916.68141
[80] Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970, pp. 466-483. Springer (1983). doi:10.1007/978-3-642-81955-1_28. ISBN 978-3-642-81955-1
[81] Urban, J., MPTP—motivation, implementation, first experiments, J. Autom. Reason., 33, 3-4, 319-339 (2004) · Zbl 1075.68081
[82] Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar Mathematical Library. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS, vol. 6327 of LNCS, pp. 155-166. Springer (2010). doi:10.1007/978-3-642-15582-6_30. ISBN 978-3-642-15581-9 · Zbl 1294.68128
[83] Urban, J., Vyskočil, J., Štěpánek, P.: MaLeCoP machine learning connection prover. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX, vol. 6793 of LNCS, pp. 263-277. Springer (2011). doi:10.1007/978-3-642-22119-4_21. ISBN 978-3-642-22118-7 · Zbl 1332.68206
[84] Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1—machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR, vol. 5195 of LNCS, pp. 441-456. Springer (2008). doi:10.1007/978-3-540-71070-7_37. ISBN 978-3-540-71069-1 · Zbl 1165.68434
[85] Veroff, R., Using hints to increase the effectiveness of an automated reasoning program: case studies, J. Autom. Reason., 16, 3, 223-239 (1996) · Zbl 0857.68095
[86] Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O., Muñoz, C.A., Tahar, S. (eds.) TPHOLs, vol. 5170 of LNCS, pp. 33-38. Springer (2008). doi:10.1007/978-3-540-71067-7_7. ISBN 978-3-540-71065-3 · Zbl 1165.68478
[87] Whalen, D.: Holophrasm: a neural automated theorem prover for higher-order logic (2016). CoRR arXiv:1608.02644
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.