{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T00:52:28Z","timestamp":1767142348431,"version":"build-2238731810"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T00:00:00Z","timestamp":1653264000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T00:00:00Z","timestamp":1653264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R026092\/1"],"award-info":[{"award-number":["EP\/R026092\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,11]]},"abstract":"Abstract<\/jats:title>\n \n We present novel reductions of extensions of the basic modal logic\n \n \n $${\\textsf {K} }$$<\/jats:tex-math>\n \n K<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n with axioms\n \n \n $$\\textsf {B} $$<\/jats:tex-math>\n \n B<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n ,\n \n \n $$\\textsf {D} $$<\/jats:tex-math>\n \n D<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n ,\n \n \n $$\\textsf {T} $$<\/jats:tex-math>\n \n T<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n ,\n \n \n $$\\textsf {4} $$<\/jats:tex-math>\n \n 4<\/mml:mn>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n and\n \n \n $$\\textsf {5} $$<\/jats:tex-math>\n \n 5<\/mml:mn>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n to Separated Normal Form with Sets of Modal Levels\n \n \n $$\\textsf {SNF} _{sml}$$<\/jats:tex-math>\n \n \n SNF<\/mml:mi>\n \n sml<\/mml:mi>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n . The reductions typically result in smaller formulae than the reductions by Kracht. The reductions to\n \n \n $$\\textsf {SNF} _{sml}$$<\/jats:tex-math>\n \n \n SNF<\/mml:mi>\n \n sml<\/mml:mi>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n combined with a reduction to\n \n \n $$\\textsf {SNF} _{ml}$$<\/jats:tex-math>\n \n \n SNF<\/mml:mi>\n \n ml<\/mml:mi>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n allow us to use the local reasoning of the prover\n \n \n $${\\text {K}_{\\text {S}}}{\\text {P}}$$<\/jats:tex-math>\n \n \n \n K<\/mml:mtext>\n S<\/mml:mtext>\n <\/mml:msub>\n P<\/mml:mtext>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n to determine the satisfiability of modal formulae in the considered logics. We show experimentally that the combination of our reductions with the prover\n \n \n $${\\text {K}_{\\text {S}}}{\\text {P}}$$<\/jats:tex-math>\n \n \n \n K<\/mml:mtext>\n S<\/mml:mtext>\n <\/mml:msub>\n P<\/mml:mtext>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n performs well when compared with a specialised resolution calculus for these logics, the built-in reductions of the first-order prover SPASS, and the higher-order logic prover LEO-III.\n <\/jats:p>","DOI":"10.1007\/s10817-022-09630-6","type":"journal-article","created":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T06:07:10Z","timestamp":1653286030000},"page":"639-666","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Local is Best: Efficient Reductions to Modal Logic K"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0310-7378","authenticated-orcid":false,"given":"Fabio","family":"Papacchini","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9792-5346","authenticated-orcid":false,"given":"Cl\u00e1udia","family":"Nalon","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0455-0267","authenticated-orcid":false,"given":"Ullrich","family":"Hustadt","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4610-9533","authenticated-orcid":false,"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,23]]},"reference":[{"key":"9630_CR1","first-page":"190","volume-title":"IJCAI 1997","author":"P Balbiani","year":"1997","unstructured":"Balbiani, P., Demri, S.: Prefixed tableaux systems for modal logics with enriched languages. In: Pollack, M.E. (ed.) IJCAI 1997, pp. 190\u2013195. Morgan Kaufmann, San Mateo (1997)"},{"issue":"3","key":"9630_CR2","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1006249507577","volume":"24","author":"P Balsiger","year":"2000","unstructured":"Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. J. Autom. Reason. 24(3), 297\u2013317 (2000). https:\/\/doi.org\/10.1023\/A:1006249507577","journal-title":"J. Autom. Reason."},{"issue":"6","key":"9630_CR3","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1093\/logcom\/7.6.685","volume":"7","author":"D Basin","year":"1997","unstructured":"Basin, D., Matthews, S., Vigano, L.: Labelled propositional modal logics: Theory and practice. J. Log. Comput. 7(6), 685\u2013717 (1997)","journal-title":"J. Log. Comput."},{"issue":"6","key":"9630_CR4","doi-asserted-by":"publisher","first-page":"881","DOI":"10.1093\/jigpal\/jzp080","volume":"18","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL 18(6), 881\u2013892 (2010)","journal-title":"Log. J. IGPL"},{"key":"9630_CR5","volume-title":"Modal Logic. Cambridge Tracts in Theoretical Computer Science","author":"P Blackburn","year":"2002","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2002)"},{"issue":"3","key":"9630_CR6","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/j.apal.2011.09.004","volume":"163","author":"M Fitting","year":"2012","unstructured":"Fitting, M.: Prefixed tableaus and nested sequents. Ann. Pure Appl. Log. 163(3), 291\u2013313 (2012)","journal-title":"Ann. Pure Appl. Log."},{"key":"9630_CR7","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0003-4843(75)90004-2","volume":"8","author":"DM Gabbay","year":"1975","unstructured":"Gabbay, D.M.: Decidability results in non-classical logics: part I. Ann. Math. Log. 8, 237\u2013295 (1975)","journal-title":"Ann. Math. Log."},{"key":"9630_CR8","doi-asserted-by":"publisher","unstructured":"Gasquet, O., Herzig, A., Longin, D., Sahade, M.: LoTREC: Logical tableaux research engineering companion. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS, vol. 3702, pp. 318\u2013322. Springer, Berlin (2005). https:\/\/doi.org\/10.1007\/11554554_25","DOI":"10.1007\/11554554_25"},{"key":"9630_CR9","doi-asserted-by":"publisher","unstructured":"Glei\u00dfner, T., Steen, A.: LEO-III (2022). https:\/\/doi.org\/10.5281\/zenodo.4435994","DOI":"10.5281\/zenodo.4435994"},{"key":"9630_CR10","doi-asserted-by":"publisher","unstructured":"Glei\u00dfner, T., Steen, A., Benzm\u00fcller, C.: Theorem provers for every normal modal logic. In: Eiter, T., Sands, D. (eds.) LPAR 2017. EPiC Series in Computing, vol.\u00a046, pp. 14\u201330. EasyChair, Maun (2017). https:\/\/doi.org\/10.29007\/jsb9","DOI":"10.29007\/jsb9"},{"key":"9630_CR11","doi-asserted-by":"publisher","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 297\u2013396. Springer, Berlin (1999). https:\/\/doi.org\/10.1007\/978-94-017-1754-0_6","DOI":"10.1007\/978-94-017-1754-0_6"},{"issue":"3","key":"9630_CR12","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"JY Halpern","year":"1992","unstructured":"Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artif. Intell. 54(3), 319\u2013379 (1992)","journal-title":"Artif. Intell."},{"issue":"1","key":"9630_CR13","first-page":"177","volume":"2","author":"A Heuerding","year":"1996","unstructured":"Heuerding, A., J\u00e4ger, G., Schwendimann, S., Seyfried, M.: The logics workbench LWB: a snapshot. Euromath Bull. 2(1), 177\u2013186 (1996)","journal-title":"Euromath Bull."},{"key":"9630_CR14","doi-asserted-by":"crossref","unstructured":"Horrocks, I., Hustadt, U., Sattler, U., Schmidt, R.A.: Computational modal logic. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, chap.\u00a04, pp. 181\u2013245. Elsevier, Amsterdam (2006)","DOI":"10.1016\/S1570-2464(07)80007-3"},{"key":"9630_CR15","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-38574-2_31","volume-title":"CADE2013","author":"M Kaminski","year":"2013","unstructured":"Kaminski, M., Tebbi, T.: InKreSAT: modal reasoning via incremental reduction to SAT. In: Bonacina, M.P. (ed.) CADE2013, pp. 436\u2013442. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_31"},{"issue":"6","key":"9630_CR16","doi-asserted-by":"publisher","first-page":"879","DOI":"10.1093\/logcom\/11.6.879","volume":"11","author":"M Kracht","year":"2001","unstructured":"Kracht, M.: Reducing modal consequence relations. J. Log. Comput. 11(6), 879\u2013907 (2001)","journal-title":"J. Log. Comput."},{"key":"9630_CR17","first-page":"243","volume-title":"Advances in Modal Logic 4","author":"M Kracht","year":"2003","unstructured":"Kracht, M.: Notes on the space requirements for checking satisfiability in modal logics. In: Balbiani, P., Suzuki, N.Y., Wolter, F., Zakaryaschev, M. (eds.) Advances in Modal Logic 4, pp. 243\u2013264. King\u2019s College Publications, London (2003)"},{"key":"9630_CR18","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1006155811656","volume":"24","author":"F Massacci","year":"2000","unstructured":"Massacci, F.: Single step tableaux for modal logics. J. Autom. Reason. 24, 319\u2013364 (2000). https:\/\/doi.org\/10.1023\/A:1006155811656","journal-title":"J. Autom. Reason."},{"key":"9630_CR19","unstructured":"Nalon, C.: $${\\text{K}_\\text{ S }}{\\text{ P }}$$ (2022). https:\/\/nalon.org\/#software"},{"key":"9630_CR20","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.jalgor.2007.04.001","volume":"62","author":"C Nalon","year":"2007","unstructured":"Nalon, C., Dixon, C.: Clausal resolution for normal modal logics. J. Algorithms 62, 117\u2013134 (2007)","journal-title":"J. Algorithms"},{"key":"9630_CR21","doi-asserted-by":"crossref","unstructured":"Nalon, C., Dixon, C., Hustadt, U.: Modal resolution: proofs, layers, and refinements. ACM Trans. Comput. Log. 20(4), 23:1\u201323:38 (2019)","DOI":"10.1145\/3331448"},{"key":"9630_CR22","doi-asserted-by":"publisher","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: $${\\text{ K}_\\text{ S }}{\\text{ P }}$$: a resolution-based prover for multimodal K. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 406\u2013415. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_28","DOI":"10.1007\/978-3-319-40229-1_28"},{"key":"9630_CR23","doi-asserted-by":"publisher","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: A modal-layered resolution calculus for K. In: de\u00a0Nivelle, H. (ed.) TABLEAUX 2015. LNCS, vol. 9323, pp. 185\u2013200. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_13","DOI":"10.1007\/978-3-319-24312-2_13"},{"issue":"3","key":"9630_CR24","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/s10817-018-09503-x","volume":"64","author":"C Nalon","year":"2020","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: $${\\text{ K}_\\text{ S }}{\\text{ P }}$$: architecture, refinements, strategies and experiments. J. Autom. Reason. 64(3), 461\u2013484 (2020). https:\/\/doi.org\/10.1007\/s10817-018-09503-x","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9630_CR25","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s11225-011-9341-3","volume":"98","author":"LA Nguyen","year":"2011","unstructured":"Nguyen, L.A., Szalas, A.: Exptime tableau decision procedures for regular grammar logics with converse. Studia Logica 98(3), 387\u2013428 (2011)","journal-title":"Studia Logica"},{"key":"9630_CR26","doi-asserted-by":"crossref","unstructured":"Ohlbach, H.J., Nonnengart, A., de\u00a0Rijke, M., Gabbay, D.M.: Encoding two-valued nonclassical logics in classical logic. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap.\u00a021, pp. 1403\u20131485. Elsevier, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50023-0"},{"key":"9630_CR27","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-08587-6_20","volume-title":"JCAR2014","author":"J Otten","year":"2014","unstructured":"Otten, J.: MleanCoP: a connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) JCAR2014. LNCS, vol. 8562, pp. 269\u2013276. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_20"},{"issue":"1\u20132","key":"9630_CR28","doi-asserted-by":"publisher","first-page":"169","DOI":"10.3166\/jancl.16.169-207","volume":"16","author":"G Pan","year":"2006","unstructured":"Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for the modal logic K. J. Appl. Non-Class. Log. 16(1\u20132), 169\u2013208 (2006)","journal-title":"J. Appl. Non-Class. Log."},{"key":"9630_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-030-79876-5_5","volume-title":"CADE 2021","author":"F Papacchini","year":"2021","unstructured":"Papacchini, F., Nalon, C., Hustadt, U., Dixon, C.: Efficient local reductions to basic modal logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS, vol. 12699, pp. 76\u201392. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_5"},{"issue":"4","key":"9630_CR30","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1023\/A:1006043519663","volume":"22","author":"RA Schmidt","year":"1999","unstructured":"Schmidt, R.A.: Decidability by resolution for propositional modal logics. J. Autom. Reason. 22(4), 379\u2013396 (1999). https:\/\/doi.org\/10.1023\/A:1006043519663","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9630_CR31","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1276920.1276921","volume":"8","author":"RA Schmidt","year":"2007","unstructured":"Schmidt, R.A., Hustadt, U.: The axiomatic translation principle for modal logic. ACM Trans. Comput. Log. 8(4), 19 (2007)","journal-title":"ACM Trans. Comput. Log."},{"key":"9630_CR32","doi-asserted-by":"publisher","unstructured":"Schmidt, R.A., Hustadt, U.: First-order resolution methods for modal logics. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics: Essays in Memory of Harald Ganzinger. LNCS, vol. 7797, pp. 345\u2013391. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-37651-1_15","DOI":"10.1007\/978-3-642-37651-1_15"},{"key":"9630_CR33","unstructured":"Schulz, S.: E 2.6 (2022). http:\/\/wwwlehre.dhbw-stuttgart.de\/~sschulz\/E\/Download.html"},{"key":"9630_CR34","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNAI, vol. 11716, pp. 495\u2013507. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"9630_CR35","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1613\/jair.2675","volume":"35","author":"R Sebastiani","year":"2009","unstructured":"Sebastiani, R., Vescovi, M.: Automated reasoning in modal and description logics via SAT encoding: the case study of K(m)\/ALC-satisfiability. J. Artif. Intell. Res. 35, 343\u2013389 (2009)","journal-title":"J. Artif. Intell. Res."},{"key":"9630_CR36","doi-asserted-by":"publisher","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: Giacomo, G.D., Catal\u00e1, A., Dilkina, B., Milano, M., Barro, S., Bugar\u00edn, A., Lang, J. (eds.) ECAI2020. Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 2937\u20132938. IOS Press, Amsterdam (2020). https:\/\/doi.org\/10.3233\/FAIA200462","DOI":"10.3233\/FAIA200462"},{"issue":"6","key":"9630_CR37","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1007\/s10817-021-09588-x","volume":"65","author":"A Steen","year":"2021","unstructured":"Steen, A., Benzm\u00fcller, C.: Extensional higher-order paramodulation in LEO-III. J. Autom. Reason. 65(6), 775\u2013807 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09588-x","journal-title":"J. Autom. Reason."},{"key":"9630_CR38","unstructured":"The SPASS Team: SPASS 3.9 (2016). http:\/\/www.spass-prover.org\/"},{"key":"9630_CR39","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning","author":"C Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965\u20132013. Elsevier and MIT Press, Cambridge (2001)"}],"updated-by":[{"DOI":"10.1007\/s10817-022-09633-3","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2022,9,14]],"date-time":"2022-09-14T00:00:00Z","timestamp":1663113600000}}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09630-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09630-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09630-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,5]],"date-time":"2022-11-05T07:19:08Z","timestamp":1667632748000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09630-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,23]]},"references-count":39,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9630"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09630-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,23]]},"assertion":[{"value":"2 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 April 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 May 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 September 2022","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s10817-022-09633-3","URL":"https:\/\/doi.org\/10.1007\/s10817-022-09633-3","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}