{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:58Z","timestamp":1759638958237,"version":"3.32.0"},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2005,5]]},"DOI":"10.1007\/s10817-005-9023-9","type":"journal-article","created":{"date-parts":[[2006,6,22]],"date-time":"2006-06-22T13:38:24Z","timestamp":1150983504000},"page":"387-423","source":"Crossref","is-referenced-by-count":20,"title":["Ordinal Arithmetic: Algorithms and Mechanization"],"prefix":"10.1007","volume":"34","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]},{"given":"Daron","family":"Vroon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,23]]},"reference":[{"key":"9023_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4376-0","volume-title":"Verification of Sequential and Concurrent Programs","author":"K. R. Apt","year":"1991","unstructured":"Apt, K. R. and Olderog, E.-R.: Verification of Sequential and Concurrent Programs, Springer, Berlin Heidelberg New York, 1991."},{"key":"9023_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F. and Nipkow, T.: Term Rewriting and All That, Cambridge University Press, Cambridge, UK, 1998."},{"key":"9023_CR3","unstructured":"Bancerek, G.: The reflection theorem, J. Formaliz. Math. 2 (1990). See URL http:\/\/megrez.mizar.org\/mirror\/JFM\/Vol2\/zf refle.html ."},{"issue":"3","key":"9023_CR4","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1023\/A:1006050629424","volume":"22","author":"J. G. Belinfante","year":"1999","unstructured":"Belinfante, J. G.: Computer proofs in G\u00f6del's class theory with equational definitions for composite and cross, J. Autom. Reason. 22(3) (1999), 311\u2013339.","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9023_CR5","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1023\/A:1006010913494","volume":"22","author":"J. G. F. Belinfante","year":"1999","unstructured":"Belinfante, J. G. F.: On computer-assisted proofs in ordinal number theory, J. Autom. Reason. 22(3) (1999), 341\u2013378.","journal-title":"J. Autom. Reason."},{"key":"9023_CR6","doi-asserted-by":"crossref","unstructured":"Belinfante, J. G. F.: Reasoning about iteration in G\u00f6del's class theory, in F. Baader (ed.), Automated Deduction-CADE-19, Proceedings of the 19th International Conference on Automated Deduction, volume 2741 of LNAI, Springer-Verlag, 2003, pp. 228\u2013242.","DOI":"10.1007\/978-3-540-45085-6_18"},{"key":"9023_CR7","doi-asserted-by":"crossref","unstructured":"Bertot, Y. and Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq'Art: The calculus of inductive constructions. Texts in Theoretical Computer Science. Springer, May 2004.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9023_CR8","volume-title":"A Computational Logic Handbook","author":"R. S. Boyer","year":"1997","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic Handbook, 2nd edition, Academic Press, New York, 1997.","edition":"2nd edition"},{"key":"9023_CR9","doi-asserted-by":"crossref","unstructured":"Brock, B., Kaufmann, M. and Moore, J S.: ACL2 theorems about commercial microprocessors, in M. Srivas and A. Camilleri (eds.), Formal Methods in Computer-Aided Design (FMCAD'96), Springer, 1996, pp. 275\u2013293.","DOI":"10.1007\/BFb0031816"},{"key":"9023_CR10","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/BF02124929","volume":"xlvi","author":"G. Cantor","year":"1895","unstructured":"Cantor, G.: Beitr\u00e4ge zur Begr\u00fcndung der transfiniten Mengenlehre, Math. Ann. xlvi (1895), 481\u2013512.","journal-title":"Math. Ann."},{"key":"9023_CR11","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01444205","volume":"xlix","author":"G. Cantor","year":"1897","unstructured":"Cantor, G.: Beitr\u00e4ge zur Bgr\u00fcndung der transfiniten Mengenlehre, Math. Ann. xlix (1897), 207\u2013246.","journal-title":"Math. Ann."},{"key":"9023_CR12","unstructured":"Cantor, G.: Contributions to the Founding of the Theory of Transfinite Numbers. Dover, 1952. Translated by Philip E. B. Jourdain."},{"key":"9023_CR13","doi-asserted-by":"crossref","first-page":"11","DOI":"10.4064\/fm-28-1-11-21","volume":"28","author":"A. Church","year":"1937","unstructured":"Church, A. and Kleene, S. C.: Formal definitions in the theory of ordinal numbers, Fundam. Math. 28 (1937), 11\u201321.","journal-title":"Fundam. Math."},{"key":"9023_CR14","unstructured":"Dennis, L. A. and Smaill, A.: Ordinal arithmetic: A case study for rippling in a higher order domain, in R. Boulton and P. Jackson (eds.), Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, volume 2152 of LNCS, Springer, 2001, pp. 185\u2013200."},{"key":"9023_CR15","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. and Okada, M.: Proof-theoritic techniques for term rewriting theory, in 3rd IEEE Symp. on Logic in Computer Science, 1988, pp. 104\u2013111.","DOI":"10.1109\/LICS.1988.5108"},{"key":"9023_CR16","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. and Reingold, E. M.: Ordinal arithmetic with list structures, in Logical Foundations of Computer Science, 1992, pp. 117\u2013126.","DOI":"10.1007\/BFb0023868"},{"key":"9023_CR17","doi-asserted-by":"crossref","unstructured":"Devlin, K.: The Joy of Sets: Fundamentals of Contemporary Set Theory, 2nd edition, Springer, New York, 1992.","DOI":"10.1007\/978-1-4899-2965-5_2"},{"key":"9023_CR18","unstructured":"Doner, J.: Definability in the extended arithmetic of ordinal numbers, Diss. Math. 96 (1972)."},{"key":"9023_CR19","doi-asserted-by":"crossref","first-page":"95","DOI":"10.4064\/fm-65-1-95-127","volume":"65","author":"J. Doner","year":"1969","unstructured":"Doner, J. and Tarski, A.: An extended arithmetic of ordinal numbers, Fundam. Math. 65 (1969), 95\u2013127.","journal-title":"Fundam. Math."},{"key":"9023_CR20","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0168-0072(91)90022-E","volume":"53","author":"J. H. Gallier","year":"1991","unstructured":"Gallier, J. H.: What's so special about Kruskal's theorem and the ordinal \u03930? A survey of some results in proof theory, Ann. Pure Appl. Logic, 53 (1991) 199\u2013260.","journal-title":"Ann. Pure Appl. Logic"},{"key":"9023_CR21","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF01565428","volume":"112","author":"G. Gentzen","year":"1936","unstructured":"Gentzen, G.: Die Widerspruchsfreiheit der reinen Zahlentheorie, Math. Ann. 112 (1936), 493\u2013565. English translation in M. E. Szabo (ed.), The Collected Works of Gerhard Gentzen, North-Holland, Amsterdam, 1969, pp. 132\u2013213.","journal-title":"Math. Ann"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","key":"9023_CR22","unstructured":"Gordon, M. J. C. and Melham, T. F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, Cambridge, UK, 1993."},{"key":"9023_CR23","doi-asserted-by":"crossref","unstructured":"Greve, D., Wilding, M. and Hardin, D.: High-speed, analyzable simulators, in Kaufmann et al. [25], 2000, pp. 113-135.","DOI":"10.1007\/978-1-4757-3188-0_8"},{"key":"9023_CR24","doi-asserted-by":"crossref","unstructured":"Greve, D. A.: Symbolic simulation of the JEM1 microprocessor, in Formal Methods in Computer-Aided Design \u2013 FMCAD, LNCS. Springer, 1998.","DOI":"10.1007\/3-540-49519-3_21"},{"key":"9023_CR25","first-page":"113","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","unstructured":"Kaufmann, M., Manolios, P. and Moore, J S. (eds.), Computer-Aided Reasoning: ACL2 Case Studies, Kluwer, Boston, MA, June 2000."},{"key":"9023_CR26","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P. and Moore, J S.: Computer-Aided Reasoning: An Approach, Kluwer, Boston, MA, July 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"9023_CR27","unstructured":"Kaufmann, M. and Moore, J S.: ACL2 homepage. See URL http:\/\/www.cs.-utexas.edu\/users\/moore\/acl2 ."},{"key":"9023_CR28","unstructured":"Kaufmann, M. and Moore, J. S. (eds.), Proceedings of the ACL2 Workshop 2000. The University of Texas at Austin, Technical Report TR-00-29, November 2000."},{"key":"9023_CR29","unstructured":"Kaufmann, M. and Moore, J. S. (eds.), Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003), July 2003. See URL http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/ ."},{"key":"9023_CR30","volume-title":"Set Theory \u2013 An Introduction to Independence Proofs, volume 102 of Studies in Logic and the Foundations of Mathematics","author":"K. Kunen","year":"1980","unstructured":"Kunen, K.: Set Theory \u2013 An Introduction to Independence Proofs, volume 102 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1980."},{"key":"9023_CR31","unstructured":"Manolios, P.: Correctness of pipelined machines, in W. A. Hunt Jr. and S. D. Johnson (eds.), Formal Methods in Computer-Aided Design \u2013 FMCAD 2000, volume 1954 of LNCS, Springer, London, UK, 2000, pp. 161\u2013178."},{"key":"9023_CR32","unstructured":"Manolios, P.: Mechanical verification of reactive systems. PhD thesis, University of Texas at Austin, August 2001. See URL http:\/\/www.cc.gatech.edu\/_manolios\/publications.html ."},{"key":"9023_CR33","unstructured":"Manolios, P. and Moore, J S.: Partial functions in ACL2, in M. Kaufmann and J S. Moore (eds.), Proceedings of the ACL2 Workshop 2000. The University of Texas at Austin, Technical Report TR-00-29, November 2000."},{"issue":"2","key":"9023_CR34","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1023\/B:JARS.0000009505.07087.34","volume":"31","author":"P. Manolios","year":"2003","unstructured":"Manolios, P. and Moore, J S.: Partial functions in ACL2, J. Autom. Reason. 31(2) (2003), 107\u2013127.","journal-title":"J. Autom. Reason."},{"key":"9023_CR35","doi-asserted-by":"crossref","unstructured":"Manolios, P., Namjoshi, K. and Sumners, R.: Linking theorem proving and model-checking with well-founded bisimulation, in N. Halbwachs and D. Peled (eds.), Computer-Aided Verification-CAV '99, volume 1633 of LNCS, Springer, 1999, pp. 369\u2013379.","DOI":"10.1007\/3-540-48683-6_32"},{"key":"9023_CR36","doi-asserted-by":"crossref","unstructured":"Manolios, P. and Vroon, D.: Algorithms for ordinal arithmetic, in F. Baader, (ed.), 19th International Conference on Automated Deduction \u2013 CADE-19, volume 2741 of LNAI, Springer, July\/August 2003, pp. 243\u2013257.","DOI":"10.1007\/978-3-540-45085-6_19"},{"key":"9023_CR37","unstructured":"Manolios, P. and Vroon, D.: Ordinal arithmetic in ACL2, in Kaufmann, M. and Moore, J S. (eds.), Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003), July 2003. See URL http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/ ."},{"key":"9023_CR38","doi-asserted-by":"crossref","unstructured":"Manolios, P. and Vroon, D.: Integrating reasoning about ordinal arithmetic into ACL2, in Formal Methods in Computer-Aided Design: 5th International Conference \u2013 FMCAD-2004, LNCS, Springer, November 2004.","DOI":"10.1007\/978-3-540-30494-4_7"},{"key":"9023_CR39","unstructured":"Medina-Bulo, I., Palomo-Lozano, F. and Alonso-Jimenez, J. A.: Implementation in ACL2 of well-founded polynomial orderings, in M. Kaufmann and J S. Moore (eds.), Proceedings of the ACL2 Workshop 2002, 2002."},{"key":"9023_CR40","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1017\/S0022481200051501","volume":"41","author":"L. W. Miller","year":"1976","unstructured":"Miller, L. W.: Normal functions and constructive ordinal notations, J. Symbolic Logic 41 (June 1976), 439\u2013459.","journal-title":"J. Symb. Logic"},{"issue":"9","key":"9023_CR41","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J S. Moore","year":"1998","unstructured":"Moore, J S., Lynch, T. and Kaufmann, M.: A mechanically checked proof of the AMD5K86 floating-point division program, IEEE Trans. Comput. 47(9) (September 1998), 913\u2013926.","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"9023_CR42","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1109\/MAHC.1984.10017","volume":"6","author":"F. Morris","year":"1984","unstructured":"Morris, F. and Jones, C.: An early program proof by Alan Turing, IEEE Ann. Hist. Comput. 6(2) (April\u2013June 1984), 139\u2013143.","journal-title":"IEEE Ann. Hist. Comput."},{"key":"9023_CR43","doi-asserted-by":"crossref","unstructured":"Owre, S. Rushby, J. and Shankar, N.: PVS: A prototype verification system, in D. Kapur (ed), 11th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, vol. 607, Springer, June 1992, pp. 748\u2013752.","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"3","key":"9023_CR44","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L. C. Paulson","year":"1993","unstructured":"Paulson, L. C.: Set theory for verification: I. From foundations to functions, J. Autom. Reason. 11(3) (1993), 353\u2013389.","journal-title":"J. Autom. Reason."},{"key":"9023_CR45","unstructured":"Paulson, L. C.: Isabelle: A Generic Theorem Prover, Springer LNCS 828, New York, NY, 1994."},{"issue":"2","key":"9023_CR46","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L. C. Paulson","year":"1995","unstructured":"Paulson, L. C.: Set theory for verification: II. Induction and recursion, J. Autom. Reason. 15(2) (1995), 167\u2013215.","journal-title":"J. Autom. Reason."},{"key":"9023_CR47","unstructured":"Paulson, L. C.: The reflection theorem: A study in meta-theoretic reasoning, in A. Voronkov (ed.), 18th International Conf. on Automated Deduction: CADE-18, number 2392 in LNAI, Springer, 2002, pp. 377\u2013391."},{"key":"9023_CR48","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1112\/S1461157000000449","volume":"6","author":"L. C. Paulson","year":"2003","unstructured":"Paulson, L. C.: The relative consistency of the axiom of choice mechanized using Isabelle, LMS J. Comput. Math. 6 (2003), 198\u2013248.","journal-title":"LMS J. Comput. Math."},{"key":"9023_CR49","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/BF00283132","volume":"17","author":"L. C. Paulson","year":"1996","unstructured":"Paulson, L. C. and Grabczewski, K.: Mechanizing set theory: Cardinal arithmetic and the axiom of choice, J. Autom. Reason. 17 (1996), 291\u2013323.","journal-title":"J. Autom. Reason."},{"key":"9023_CR50","unstructured":"Rogers Jr, H.: Theory of Recursive Functions and Effective Computability, MIT Press, Cambridge, MA, 1987."},{"key":"9023_CR51","unstructured":"Rudnicki, P.: An overview of the MIZAR project, in 1992 Workshop on Types for Proofs and Programs, 1992."},{"key":"9023_CR52","unstructured":"Ruiz-Reina, J.-L., Alonso, J.-A., Hidalgo, M.-J. and Martin, F.-J.: Multiset relations: A tool for proving termination, in Kaufmann, M. and Moore, J S. (eds.), Proceedings of the ACL2 Workshop 2000, The University of Texas at Austin, Technical Report TR-00-29, November 2000."},{"key":"9023_CR53","unstructured":"Russinoff, D. M.: A mechanically checked proof of correctness of the AMD5K86 floating-point square root microcode, Formal Methods in System Design Special Issue on Arithmetic Circuits, 1997."},{"key":"9023_CR54","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. M. Russinoff","year":"1998","unstructured":"Russinoff, D. M.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions, LMS J. Comput. Math. 1 (December 1998), 148\u2013200.","journal-title":"LMS J. Comput. Math."},{"key":"9023_CR55","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1023\/A:1008669628911","volume":"14","author":"D. M. Russinoff","year":"1999","unstructured":"Russinoff, D. M.: A mechanically checked proof of correctness of the AMDK5 floating-point square root microcode, Form. Methods Syst. Des. 14 (1999), 75\u2013125.","journal-title":"Form. Methods Syst. Des."},{"key":"9023_CR56","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-1-4757-3188-0_13","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"D. M. Russinoff","year":"2000","unstructured":"Russinoff, D. M. and Flatau, A.: RTL verification: A floating-point multiplier, Kaufmann, M., Manolios, P. and Moore, J S. (eds.), Computer-Aided Reasoning: ACL2 Case Studies, Kluwer, Boston, MA, 2000, pp. 201\u2013231."},{"key":"9023_CR57","doi-asserted-by":"crossref","unstructured":"Sch\u00fctte, K.: Proof Theory. Springer, 1977. Translation from German by J. N. Crossley. The book is a completely rewritten version of Beweistheorie, Springer, 1960.","DOI":"10.1007\/978-3-642-66473-1"},{"key":"9023_CR58","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1017\/CBO9781107325944.013","volume-title":"Sets and Proofs","author":"A. Setzer","year":"1999","unstructured":"Setzer, A.: Ordinal systems, in B. Cooper and J. Truss (eds.), Sets and Proofs, Cambridge University Press, Cambridge, 1999, pp. 301\u2013331."},{"key":"9023_CR59","doi-asserted-by":"crossref","unstructured":"Setzer, A.: Ordinal systems part 2: One inaccessible, in Logic Colloquium '98, volume 13 of ASL Lecture Notes in Logic, 2000, pp. 426\u2013448.","DOI":"10.1017\/9781316756140.030"},{"key":"9023_CR60","unstructured":"Sumners, R.: An incremental stuttering refinement proof of a concurrent program in ACL2, in Kaufmann, M. and Moore, J S. (eds.), Proceedings of the ACL2 Workshop 2000. The University of Texas at Austin, Technical Report TR-00-29, November 2000."},{"key":"9023_CR61","unstructured":"Sustik, M.: Proof of Dixon's lemma using the ACL2 theorem prover via an explicit ordinal mapping, in Kaufmann, M. and Moore, J S. (eds.), Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003), July 2003. See URL http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/ ."},{"key":"9023_CR62","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"A. S. Troelstra","year":"2000","unstructured":"Troelstra, A. S. and Schwichtenberg, H.: Basic Proof Theory, 2nd edition, Cambridge University Press, Cambridge, 2000.","edition":"2nd edition"},{"issue":"2","key":"9023_CR63","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1112\/plms\/s2-45.1.161","volume":"45","author":"A. M. Turing","year":"1939","unstructured":"Turing, A. M.: Systems of logic based on ordinals, Proc. Lond. Math. Soc. 45(2) (1939), 161\u2013228. See URL http:\/\/www.- turingarchive.org\/ .","journal-title":"Proc. Lond. Math. Soc."},{"key":"9023_CR64","unstructured":"Turing, A. M.: Checking a large routine, in Report of a Conference on High Speed Automatic Calculating Machines, University Mathematical Laboratory, Cambridge, June 1949, pp. 67\u201369."},{"key":"9023_CR65","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1090\/S0002-9947-1908-1500814-9","volume":"9","author":"O. Veblen","year":"1908","unstructured":"Veblen, O.: Continuous increasing functions of finite and transfinite ordinals, Trans. Am. Math. Soc. 9 (1908), 280\u2013292.","journal-title":"Trans. Am. Math. Soc."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9023-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-005-9023-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9023-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T14:38:33Z","timestamp":1736433513000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-005-9023-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":65,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,5]]}},"alternative-id":["9023"],"URL":"https:\/\/doi.org\/10.1007\/s10817-005-9023-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2005,5]]}}}