{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:03:36Z","timestamp":1777424616892,"version":"3.51.4"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T00:00:00Z","timestamp":1465862400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Universidad de La Rioja","award":["FPI-UR-12"],"award-info":[{"award-number":["FPI-UR-12"]}]},{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad (ES)","doi-asserted-by":"publisher","award":["MTM2014-54151-P"],"award-info":[{"award-number":["MTM2014-54151-P"]}],"id":[{"id":"10.13039\/501100003329","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":[[2017,4]]},"DOI":"10.1007\/s10817-016-9379-z","type":"journal-article","created":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T07:48:37Z","timestamp":1465890517000},"page":"509-535","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4079-8307","authenticated-orcid":false,"given":"Jes\u00fas","family":"Aransay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jose","family":"Divas\u00f3n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,14]]},"reference":[{"key":"9379_CR1","unstructured":"Adelsberger, S., Hetzl, S., Pollak, F.: The Cayley\u2013Hamilton theorem. Arch. Form. Proofs (2014). http:\/\/afp.sf.net\/entries\/Cayley_Hamilton.shtml , Formal proof development"},{"issue":"1","key":"9379_CR2","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1017\/S0956796812000019","volume":"22","author":"K Aehlig","year":"2012","unstructured":"Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of normalization by evaluation. J. Funct. Program. 22(1), 9\u201330 (2012)","journal-title":"J. Funct. Program."},{"key":"9379_CR3","doi-asserted-by":"crossref","unstructured":"Afshar, S.K., Aravantinos, V., Hasan, O., Tahar, S.: Formalization of complex vectors in higher-order logic. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics: CICM 2014. Proceedings, Lecture Notes in Artificial Intelligence, vol. 8543, pp. 123\u2013137. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-08434-3_10"},{"key":"9379_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-319-14125-1_1","volume-title":"Post Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation: LOPSTR 2013","author":"J Aransay","year":"2014","unstructured":"Aransay, J., Divas\u00f3n, J.: Formalization and execution of linear algebra: from theorems to algorithms. In: Gupta, G., Pe\u00f1a, R. (eds.) Post Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation: LOPSTR 2013. Lecture Notes in Computer Science, vol. 8901, pp. 1\u201319. Springer, Berlin (2014)"},{"key":"9379_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796815000155","volume":"25","author":"J Aransay","year":"2015","unstructured":"Aransay, J., Divas\u00f3n, J.: Formalisation in higher-order logic and code generation to functional languages of the Gauss\u2013Jordan algorithm. J. Funct. Program. 25, 1\u201321 (2015)","journal-title":"J. Funct. Program."},{"key":"9379_CR6","doi-asserted-by":"crossref","unstructured":"Aransay, J., Divas\u00f3n, J.: Generalizing a mathematical analysis library in Isabelle\/HOL. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NASA Formal Methods: NFM 2015, Lecture Notes in Computer Science, vol. 9508, pp. 415\u2013421. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-17524-9_30"},{"key":"9379_CR7","doi-asserted-by":"crossref","unstructured":"Aransay, J., Divas\u00f3n, J.: Formalisation of the computation of the Echelon form of a matrix in Isabelle\/HOL. Form. Asp. Comput. (accepted for publication) (2016)","DOI":"10.1007\/s00165-016-0383-1"},{"key":"9379_CR8","unstructured":"Aransay, J., Divas\u00f3n, J.: Verified Computer Linear Algebra. Accepted for Publication in the Conference EACA 2016 (2016). https:\/\/www.unirioja.es\/cu\/jearansa\/archivos\/vcla.pdf"},{"key":"9379_CR9","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rck, A.: Numerical Methods for Least Squares Problems. SIAM (1996)","DOI":"10.1137\/1.9781611971484"},{"key":"9379_CR10","doi-asserted-by":"crossref","unstructured":"Blanchette, J., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber, M. (ed.) Conference on Intelligent Computer Mathematics: CICM 2015, Lecture Notes in Computer Science, vol. 9150, pp. 3\u201317. Springer, Berlin (2015). Invited paper","DOI":"10.1007\/978-3-319-20615-8_1"},{"issue":"2","key":"9379_CR11","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/s10817-014-9317-x","volume":"54","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Jourdan, J., Leroy, X., Melquiond, G.: Verified compilation of floating-point computations. J. Autom. Reason. 54(2), 135\u2013163 (2015)","journal-title":"J. Autom. Reason."},{"key":"9379_CR12","doi-asserted-by":"publisher","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. FirstView, 1\u201338 (2016). doi: 10.1017\/S0960129514000437 . http:\/\/journals.cambridge.org\/articleS0960129514000437","DOI":"10.1017\/S0960129514000437"},{"key":"9379_CR13","unstructured":"Butler, R.B.: Formalization of the Integral Calculus in the PVS Theorem Prover. Tech. Rep. NASA\/TM-2004-213279, L-18391, NASA Langley Research Center (2004). http:\/\/ntrs.nasa.gov\/search.jsp?R=20040171869"},{"key":"9379_CR14","unstructured":"Chang, W., Yamazaki, H., Nakamura, Y.: A theory of matrices of complex elements. Form. Math. 13(1), 157\u2013162 (2005). http:\/\/fm.mizar.org\/2005-13\/pdf13-1\/matrix_5.pdf"},{"key":"9379_CR15","unstructured":"Chang, W., Yamazaki, H., Nakamura, Y.: The inner product and conjugate of matrix of complex numbers. Form. Math. 13(4), 493\u2013499 (2005). http:\/\/fm.mizar.org\/2005-13\/pdf13-4\/matrixc1.pdf"},{"key":"9379_CR16","doi-asserted-by":"crossref","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free! In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs: CPP 2013, Lecture Notes in Computer Science, vol. 8307, pp. 147\u2013162. Springer, Berlin (2013)","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"9379_CR17","doi-asserted-by":"crossref","unstructured":"Dahlquist, G., Bj\u00f6rck, A.: Numerical Methods in Scientific Computing. SIAM (2008)","DOI":"10.1137\/1.9780898717785"},{"issue":"2","key":"9379_CR18","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1109\/TC.2008.213","volume":"58","author":"M Daumas","year":"2009","unstructured":"Daumas, M., Lester, D., Mu\u00f1oz, C.: Verified real number calculations: a library for interval arithmetic. IEEE Trans. Comput. 58(2), 226\u2013237 (2009)","journal-title":"IEEE Trans. Comput."},{"key":"9379_CR19","doi-asserted-by":"crossref","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in COQ. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving: ITP 2012, Lecture Notes in Computer Science, vol. 7406, pp. 83\u201398. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"9379_CR20","unstructured":"Divas\u00f3n, J., Aransay, J.: Rank\u2013Nullity theorem in linear algebra. Arch. Form. Proofs (2013). http:\/\/afp.sf.net\/entries\/Rank_Nullity_Theorem.shtml"},{"key":"9379_CR21","unstructured":"Divas\u00f3n, J., Aransay, J.: Gauss\u2013Jordan algorithm and its applications. Arch. Form. Proofs (2014). http:\/\/afp.sf.net\/entries\/Gauss_Jordan.shtml , Formal proof development"},{"key":"9379_CR22","unstructured":"Divas\u00f3n, J., Aransay, J.: Echelon form. Arch. Form. Proofs (2015). http:\/\/afp.sf.net\/entries\/EchelonForm.shtml , Formal proof development"},{"key":"9379_CR23","unstructured":"Divas\u00f3n, J., Aransay, J.: $$QR$$ Q R decomposition. Arch. Form. Proofs (2015). http:\/\/afp.sf.net\/entries\/QRDecomposition.shtml , Formal proof development. Updated version available from http:\/\/afp.sf.net\/devel-entries\/QRDecomposition.shtml"},{"key":"9379_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/BFb0105402","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs 97","author":"B Dutertre","year":"1996","unstructured":"Dutertre, B.: Elements of mathematical analysis in PVS. In: von Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics: TPHOLs 97. Lecture Notes in Computer Science, vol. 1125, pp. 141\u2013156. Springer, Turku (1996)"},{"key":"9379_CR25","unstructured":"Gallego-Arias, E.J., Jouvelot, P.: Adventures in the (Not So) Complex Space. The Coq Workshop 2015 (2015). https:\/\/github.com\/ejgallego\/mini-dft-coq"},{"key":"9379_CR26","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: Point-free, set-free concrete linear algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving: ITP 2011, Lecture Notes in Computer Science, vol. 6898, pp. 103\u2013118. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22863-6_10"},{"key":"9379_CR27","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O\u2019Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: Blanzy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving: ITP 2013, Lecture Notes in Computer Science, vol. 7998, pp. 163\u2013179. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"9379_CR28","unstructured":"Haftmann, F.: Code Generation from Isabelle\/HOL Theories. http:\/\/isabelle.in.tum.de\/doc\/codegen.pdf (2016)"},{"key":"9379_CR29","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Krauss, A., Kuncar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving: ITP 2013, Lecture Notes in Computer Science, vol. 7998, pp. 100\u2013115. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"9379_CR30","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming: FLOPS 2010, Lecture Notes in Computer Science, vol. 6009, pp. 103\u2013117. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"9379_CR31","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) Types for Proofs and Programs: TYPES 2006, Revised Selected Papers, Lecture Notes in Computer Science, vol. 4502, pp. 160\u2013174. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-74464-1_11"},{"key":"9379_CR32","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, D., 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. http:\/\/arxiv.org\/abs\/1501.02155 (2015)"},{"key":"9379_CR33","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics: TPHOLS 2005, Lecture Notes in Computer Science, vol. 3603, pp. 114\u2013129. Springer, Berlin (2005)","DOI":"10.1007\/11541868_8"},{"issue":"2","key":"9379_CR34","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL light theory of euclidean space. J. Autom. Reason. 50(2), 173\u2013190 (2013)","journal-title":"J. Autom. Reason."},{"key":"9379_CR35","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: Reis, G.D., Th\u00e9ry, L. (eds.) International Workshop on Programming Languages for Mechanized Mathematics Systems: PLMMS\u201909, pp. 38\u201345. Munich (2009)"},{"key":"9379_CR36","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving: ITP 2013, Lecture Notes in Computer Science, vol. 7998, pp. 279\u2013294. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"9379_CR37","unstructured":"HOL Multivariate Analysis Library. http:\/\/isabelle.in.tum.de\/library\/HOL\/HOL-Multivariate_Analysis\/index.html (2016)"},{"key":"9379_CR38","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs: CPP 2013, Lecture Notes in Computer Science, vol. 8307, pp. 131\u2013146. Springer, Berlin (2013)","DOI":"10.1007\/978-3-319-03545-1_9"},{"issue":"6","key":"9379_CR39","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"9379_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-642-39634-2_9","volume-title":"Interactive Theorem Proving: ITP 2013","author":"P Lammich","year":"2013","unstructured":"Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving: ITP 2013. Lecture Notes in Computer Science, vol. 7998, pp. 84\u201399. Springer, Berlin (2013)"},{"key":"9379_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-540-71067-7_19","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs 08","author":"DR Lester","year":"2008","unstructured":"Lester, D.R.: Real number calculations and theorem proving. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) Theorem Proving in Higher Order Logics: TPHOLs 08. Lecture Notes in Computer Science, vol. 5170, pp. 215\u2013229. Springer, Berlin (2008)"},{"key":"9379_CR42","doi-asserted-by":"publisher","unstructured":"Martin-Dorel, \u00c9., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reason. 1\u201331 (2015). doi: 10.1007\/s10817-015-9350-4","DOI":"10.1007\/s10817-015-9350-4"},{"key":"9379_CR43","unstructured":"Mathematica\u00a010.4. Wolfram Research, Inc. Champaign, IL (2016)"},{"key":"9379_CR44","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283. Springer, Berlin (2002). Updated version available in http:\/\/isabelle.in.tum.de\/doc\/tutorial.pdf","DOI":"10.1007\/3-540-45949-9"},{"key":"9379_CR45","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/s10472-009-9168-z","volume":"56","author":"S Obua","year":"2009","unstructured":"Obua, S., Nipkow, T.: Flyspeck II: the basic linear programs. Ann. Math. Artif. Intell. 56, 245\u2013272 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"4","key":"9379_CR46","doi-asserted-by":"publisher","first-page":"297","DOI":"10.2478\/v10037-008-0036-9","volume":"16","author":"K P\u0105k","year":"2008","unstructured":"P\u0105k, K.: Jordan matrix decomposition. Form. Math. 16(4), 297\u2013303 (2008). doi: 10.2478\/v10037-008-0036-9","journal-title":"Form. Math."},{"key":"9379_CR47","doi-asserted-by":"crossref","unstructured":"Solovyev, A., Hales, T.: Efficient formal verification of bounds of linear programs. In: Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 6824, pp. 123\u2013132. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22673-1_9"},{"key":"9379_CR48","doi-asserted-by":"crossref","unstructured":"Solovyev, A., Hales, T.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: NASA Formal Methods, Lecture Notes in Computer Science, vol. 7871, pp. 383\u2013397. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38088-4_26"},{"issue":"9","key":"9379_CR49","doi-asserted-by":"crossref","first-page":"848","DOI":"10.2307\/2324660","volume":"100","author":"G Strang","year":"1993","unstructured":"Strang, G.: The fudamental theorem of linear algebra. Am. Math. Mon. 100(9), 848\u2013855 (1993)","journal-title":"Am. Math. Mon."},{"key":"9379_CR50","volume-title":"Introduction to Linear Algebra","author":"G Strang","year":"2009","unstructured":"Strang, G.: Introduction to Linear Algebra, 4th edn. Wellesley-Cambridge Press, Cambridge (2009)","edition":"4"},{"key":"9379_CR51","unstructured":"Thiemann, R.: Implementing field extensions of the form $$\\mathbb{Q} [\\sqrt{b}]$$ Q [ b ] . Arch. Form. Proofs (2014). http:\/\/afp.sf.net\/entries\/Real_Impl.shtml , Formal proof development"},{"key":"9379_CR52","unstructured":"Thiemann, R., Yamada, A.: Matrices, Jordan normal forms, and spectral radius theory. Arch. Form. Proofs (2015). http:\/\/afp.sf.net\/entries\/Jordan_Normal_Form.shtml , Formal proof development"},{"key":"9379_CR53","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A.: Algebraic Numbers in Isabelle\/HOL (2016). Accepted for presentation in ITP 2016","DOI":"10.1007\/978-3-319-43144-4_24"},{"key":"9379_CR54","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014A Versatile Environment for Human-Readable Formal Proof Documents. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2002). https:\/\/mediatum.ub.tum.de\/doc\/601724\/601724.pdf"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9379-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9379-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9379-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9379-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T14:39:25Z","timestamp":1568039965000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9379-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,14]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,4]]}},"alternative-id":["9379"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9379-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6,14]]}}}