{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T12:37:37Z","timestamp":1754397457008},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_7","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T14:42:14Z","timestamp":1277822534000},"page":"82-97","source":"Crossref","is-referenced-by-count":11,"title":["Integrating Reasoning About Ordinal Arithmetic into ACL2"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]},{"given":"Daron","family":"Vroon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science\u00a0236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"7_CR2","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)"},{"issue":"1","key":"7_CR3","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/321864.321875","volume":"22","author":"R.S. Boyer","year":"1975","unstructured":"Boyer, R.S., Moore, J.S.: Proving theorems about pure lisp functions. JACM\u00a022(1), 129\u2013144 (1975)","journal-title":"JACM"},{"key":"7_CR4","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, New York (1979)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.A. Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"key":"7_CR7","unstructured":"Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Workshop on Advanced Verification (July 2000), See \n                  \n                    http:\/\/www.cs.utah.edu\/wave\/"},{"key":"7_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-540-45085-6_4","volume-title":"Automated Deduction \u2013 CADE-19","author":"N. Hirokawa","year":"2003","unstructured":"Hirokawa, N., Middledorp, A.: Automating the dependency pair method. In: Automated Deduction \u2013 CADE-19. LNCS (LNAI), pp. 32\u201346. Springer, Heidelberg (2003)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification \u2013 CAV 1998","year":"1998","unstructured":"Hu, A.J., Vardi, M.Y. (eds.): Computer-Aided Verification \u2013 CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","key":"7_CR10","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"7_CR11","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":"7_CR12","unstructured":"Kaufmann, M., Moore, J.S.: ACL2 homepage. See, \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2"},{"key":"7_CR13","unstructured":"Kaufmann, M., Moore, J.S. (eds.): Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003) (July 2003), See \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/"},{"key":"7_CR14","first-page":"81","volume":"28","author":"C.S. Lee","year":"2001","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. ACM Symposium on Principles of Programming Languages\u00a028, 81\u201392 (2001)","journal-title":"ACM Symposium on Principles of Programming Languages"},{"key":"7_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-45085-6_19","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Manolios","year":"2003","unstructured":"Manolios, P., Vroon, D.: Algorithms for ordinal arithmetic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 243\u2013257. Springer, Heidelberg (2003)"},{"key":"7_CR16","unstructured":"Manolios, P., Vroon, D.: Ordinal arithmetic in ACL2. In: Kaufmann and Moore [13], See \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-39813-4_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F.-J. Mart\u00edn-Mateos","year":"2003","unstructured":"Mart\u00edn-Mateos, F.-J., Alonso, J.-A., Hidalgo, M.-J., Ruiz-Reina, J.-L.: A formal proof of Dickson\u2019s Lemma in ACL2. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, pp. 49\u201358. Springer, Heidelberg (2003)"},{"issue":"2","key":"7_CR18","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/MAHC.1984.10017","volume":"6","author":"F. Morris","year":"1984","unstructured":"Morris, F., Jones, C.: An early program proof by Alan Turing. IEEE Annals of the History of Computing\u00a06(2), 139\u2013143 (1984)","journal-title":"IEEE Annals of the History of Computing"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelske","year":"2004","unstructured":"Podelske, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"7_CR20","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.) Proceedings of the ACL2 Workshop 2000. The University of Texas at Austin, Technical Report TR-00-29 (November 2000)"},{"key":"7_CR21","unstructured":"Sustik, M.: Proof of Dixon\u2019s lemma using the ACL2 theorem prover via an explicit ordinal mapping. In: Kaufmann and Moore [13], See \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/"},{"issue":"3","key":"7_CR22","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1023\/A:1011217102270","volume":"18","author":"M. Wilding","year":"2001","unstructured":"Wilding, M., Greve, D., Hardin, D.: Efficient simulation of formal processor models. Formal Methods in System Design\u00a018(3), 233\u2013248 (2001)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:25:57Z","timestamp":1558279557000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}