{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T12:16:09Z","timestamp":1754396169007,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_19","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"243-257","source":"Crossref","is-referenced-by-count":18,"title":["Algorithms for Ordinal Arithmetic"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]},{"given":"Daron","family":"Vroon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Beckmann, A., Buss, S.R., Pollett, C.: Ordinal notations and well-orderings in bounded arithmetic. Annals of Pure and Applied Logic, 197\u2013223 (2003)","DOI":"10.1016\/S0168-0072(02)00066-0"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0031816","volume-title":"Formal Methods in Computer-Aided Design","author":"B. Brock","year":"1996","unstructured":"Brock, B., Kaufmann, M., Moore, J.S.: ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 275\u2013293. Springer, Heidelberg (1996)"},{"key":"19_CR4","doi-asserted-by":"publisher","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. Mathematische Annalen\u00a0xlvi, 481\u2013512 (1895)","journal-title":"Mathematische Annalen"},{"key":"19_CR5","doi-asserted-by":"publisher","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. Mathematische Annalen\u00a0xlix, 207\u2013246 (1897)","journal-title":"Mathematische Annalen"},{"key":"19_CR6","volume-title":"Contributions to the Founding of the Theory of Transfinite Numbers","author":"G. Cantor","year":"1952","unstructured":"Cantor, G.: Contributions to the Founding of the Theory of Transfinite Numbers. Dover Publications, Inc., New York (1952); Translated by P.E.B. Jourdain"},{"key":"19_CR7","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., Kleene, S.C.: Formal definitions in the theory of ordinal numbers. Fundamenta mathematicae\u00a028, 11\u201321 (1937)","journal-title":"Fundamenta mathematicae"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/3-540-56610-4_68","volume-title":"TAPSOFT \u201993: Theory and Practice of Software Development","author":"N. Dershowitz","year":"1993","unstructured":"Dershowitz, N.: Trees, ordinals, and termination. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol.\u00a0668, pp. 243\u2013250. Springer, Heidelberg (1993)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Okada, M.: Proof-theoritic techniques for term rewriting theory. In: 3rd IEEE Symp. on Logic in Computer Science, pp. 104\u2013111 (1988)","DOI":"10.1109\/LICS.1988.5108"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Reingold, E.M.: Ordinal arithmetic with list structures. In: Logical Foundations of Computer Science, pp. 117\u2013126 (1992)","DOI":"10.1007\/BFb0023868"},{"key":"19_CR11","volume-title":"The Joy of Sets: Fundamentals of Contemporary Set Theory","author":"K. Devlin","year":"1992","unstructured":"Devlin, K.: The Joy of Sets: Fundamentals of Contemporary Set Theory, 2nd edn. Springer, Heidelberg (1992)","edition":"2"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Gallier, J.H.: What\u2019s so special about Kruskal\u2019s theorem and the ordinal \u03930? A survey of some results in proof theory. Annals of Pure and Applied Logic, 199\u2013260 (1991)","DOI":"10.1016\/0168-0072(91)90022-E"},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/BF01565428","volume":"112","author":"G. Gentzen","year":"1936","unstructured":"Gentzen, G.: Die widerspruchsfreiheit der reinen zahlentheorie. Mathematische Annalen\u00a0112, 493\u2013565 (1936); English translation in Szabo, M. E. (ed.) The Collected Works of Gerhard Gentzen, pp. 132\u2013213. North Holland, Amsterdam (1969)","journal-title":"Mathematische Annalen"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-49519-3_21","volume-title":"Formal Methods in Computer-Aided Design","author":"D.A. Greve","year":"1998","unstructured":"Greve, D.A.: Symbolic simulation of the JEM1 microprocessor. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 321\u2013333. Springer, Heidelberg (1998)"},{"key":"19_CR15","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"19_CR16","unstructured":"Kaufmann, M., Moore, J.S.: ACL2 homepage, See URL http:\/\/www.cs.utexas.edu\/users\/moore\/acl2"},{"key":"19_CR17","unstructured":"Kaufmann, M., Moore, J.S. (eds.): Proceedings of the ACL2 Workshop 2000. The University of Texas at Austin, Technical Report TR-00-29 (November 2000)"},{"key":"19_CR18","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Set Theory - an Introduction to Independence Proofs","author":"K. Kunen","year":"1980","unstructured":"Kunen, K.: Set Theory - an Introduction to Independence Proofs. Studies in Logic and the Foundations of Mathematics, vol.\u00a0102. North-Holland, Amsterdam (1980)"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-40922-X_11","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Manolios","year":"2000","unstructured":"Manolios, P.: Correctness of pipelined machines. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 161\u2013178. Springer, Heidelberg (2000)"},{"key":"19_CR20","unstructured":"Manolios, P.: Mechanical Verification of Reactive Systems. PhD thesis, University of Texas at Austin (August 2001)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48683-6_32","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"1999","unstructured":"Manolios, P., Namjoshi, K., Sumners, R.: Linking theorem proving and modelchecking with well-founded bisimulation. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 369\u2013379. Springer, Heidelberg (1999)"},{"key":"19_CR22","unstructured":"Manolios, P., Vroon, D.: Ordinal arithmetic in ACL2. Submitted to the 4th International Workshop on the ACL2 Theorem Prover and Its Applications (2003)"},{"key":"19_CR23","unstructured":"Medina-Bulo, I., Palomo-Lozano, F., Alonso-Jimenez, J.A.: Implementation in ACL2 of well-founded polynomial orderings. In: Kaufmann, M., Moore, J.S. (eds.) Proceedings of the ACL2 Workshop 2002 (2002)"},{"key":"19_CR24","doi-asserted-by":"publisher","first-page":"439","DOI":"10.2307\/2272243","volume":"41","author":"L.W. Miller","year":"1976","unstructured":"Miller, L.W.: Normal functions and constructive ordinal notations. Journal of Symbolic Logic\u00a041, 439\u2013459 (1976)","journal-title":"Journal of Symbolic Logic"},{"issue":"9","key":"19_CR25","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the AMD5 K 86 floating-point division program. IEEE Trans. Comp.\u00a047(9), 913\u2013926 (1998)","journal-title":"IEEE Trans. Comp."},{"key":"19_CR26","volume-title":"Theory of Recursive Functions and Effective Computability","author":"H. Rogers Jr.","year":"1987","unstructured":"Rogers Jr., H.: Theory of Recursive Functions and Effective Computability, 1st paperback edn. MIT Press, Cambridge (1987)","edition":"1"},{"key":"19_CR27","unstructured":"Ruiz-Reina, J.-L., Alonso, J.-A., Hidalgo, M.-J., Martin, F.-J.: Multiset relations: A tool for proving termination. In: Kaufmann, M., Moore, J.S. (eds.) [17]"},{"key":"19_CR28","first-page":"148","volume":"1","author":"D.M. Russinoff","year":"1998","unstructured":"Russinoff, D.M.: A mechanically checked proof of IEEE compliance of a registertransfer- level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. London Mathematical Society Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998)","journal-title":"London Mathematical Society Journal of Computation and Mathematics"},{"key":"19_CR29","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-66473-1","volume-title":"Proof Theory","author":"K. Sch\u00fctte","year":"1977","unstructured":"Sch\u00fctte, K.: Proof Theory. Springer, Heidelberg (1977); Translated by J. N. Crossley from the revised version of Beweistheorie, 1st edn. (1960)"},{"key":"19_CR30","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: Cooper, B., Truss, J. (eds.) Sets and Proofs, pp. 301\u2013331. Cambridge University Press, Cambridge (1999)"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Setzer, A.: Ordinal systems part 2: One inaccessible. In: Logic Colloquium 1998. ASL Lecture Notes in Logic, vol.\u00a013, pp. 426\u2013448 (2000)","DOI":"10.1017\/9781316756140.030"},{"key":"19_CR32","unstructured":"Sumners, R.: An incremental stuttering refinement proof of a concurrent program in ACL2. In: Kaufmann, M., Moore, J. (eds.) [17]"},{"key":"19_CR33","unstructured":"Sustik, M.: Proof of Dixon\u2019s lemma using the ACL2 theorem prover via an explicit ordinal mapping 2003. In: Submitted to the 4th International Workshop on the ACL2 Theorem Prover and Its Applications (2003)"},{"key":"19_CR34","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"A.S. Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)","edition":"2"},{"key":"19_CR35","doi-asserted-by":"publisher","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. Transactions of the American Mathematical Society\u00a09, 280\u2013292 (1908)","journal-title":"Transactions of the American Mathematical Society"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T07:31:31Z","timestamp":1740641491000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}