{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T11:16:51Z","timestamp":1778757411592,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540252368","type":"print"},{"value":"9783540322757","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_17","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:14:41Z","timestamp":1292879681000},"page":"240-256","source":"Crossref","is-referenced-by-count":5,"title":["The Equational Theory of \u2329\u2115, 0, 1,\u2009+\u2009, \u00d7, \u2191\u232a Is Decidable, but Not Finitely Axiomatisable"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Di Cosmo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Dufour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","volume-title":"LICS","author":"V. Balat","year":"2002","unstructured":"Balat, V., Di Cosmo, R., Fiore, M.: Remarks on isomorphisms in typed lambda calculi with empty and sum type. In: LICS, July 2002, IEEE, Los Alamitos (2002)"},{"key":"17_CR2","first-page":"64","volume-title":"31st Ann. ACM Symp. on Principles of Programming Languages (POPL)","author":"V. Balat","year":"2004","unstructured":"Balat, V., Di Cosmo, R., Fiore, M.: Extensional normalisation and type-directed partial evaluation for typed lamda calculus with sums. In: 31st Ann. ACM Symp. on Principles of Programming Languages (POPL), pp. 64\u201376. ACM, New York (2004)"},{"key":"17_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2572-0","volume-title":"Isomorphisms of types: from \u03bb-calculus to information retrieval and language design","author":"R. Cosmo Di","year":"1995","unstructured":"Di Cosmo, R.: Isomorphisms of types: from \u03bb-calculus to information retrieval and language design. Birkh\u00e4user, Basel (1995)"},{"issue":"6","key":"17_CR4","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1017\/S0960129596002241","volume":"7","author":"K. Dosen","year":"1997","unstructured":"Dosen, K., Petric, Z.: Isomorphic objects in symmetric monoidal closed categories. Mathematical Structures in Computer Science\u00a07(6), 639\u2013662 (1997)","journal-title":"Mathematical Structures in Computer Science"},{"key":"17_CR5","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., Tarski, A.: An extended arithmetic of ordinal numbers. Fundamenta Mathematica\u00a065, 95\u2013127 (1969)","journal-title":"Fundamenta Mathematica"},{"issue":"1","key":"17_CR6","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1090\/S0002-9939-1985-0781071-1","volume":"94","author":"R. Gurevi\u010d","year":"1985","unstructured":"Gurevi\u010d, R.: Equational theory of positive numbers with exponentiation. Proceedings of the American Mathematical Society\u00a094(1), 135\u2013141 (1985)","journal-title":"Proceedings of the American Mathematical Society"},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0168-0072(90)90049-8","volume":"49","author":"R. Gurevi\u010d","year":"1990","unstructured":"Gurevi\u010d, R.: Equational theory of positive numbers with exponentiation is not finitely axiomatizable. Annals of Pure and Applied Logic\u00a049, 1\u201330 (1990)","journal-title":"Annals of Pure and Applied Logic"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"597","DOI":"10.2307\/2321009","volume":"84","author":"L. Henkin","year":"1977","unstructured":"Henkin, L.: The logic of equality. American Mathematical Monthly\u00a084, 597\u2013612 (1977)","journal-title":"American Mathematical Monthly"},{"issue":"1","key":"17_CR9","first-page":"1","volume":"282","author":"C.W. Henson","year":"1984","unstructured":"Henson, C.W., Rubel, L.A.: Some applications of Nevanlinna theory to mathematical logic: Identities of exponential functions. Trans. Am. Math. Soc.\u00a0282(1), 1\u201332 (1984)","journal-title":"Trans. Am. Math. Soc."},{"key":"17_CR10","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/BFb0095664","volume-title":"Model Theory and Arithmetic","author":"A. Macintyre","year":"1981","unstructured":"Macintyre, A.: The laws of exponentiation. In: Berline, C., McAloon, K., Ressayre, J.-P. (eds.) Model Theory and Arithmetic. Lecture Notes in Mathematics, vol.\u00a0890, pp. 185\u2013197. Springer, Heidelberg (1981)"},{"issue":"7","key":"17_CR11","first-page":"778","volume":"19","author":"C.F. Martin","year":"1972","unstructured":"Martin, C.F.: Axiomatic bases for equational theories of natural numbers. Notices of the Am. Math. Soc.\u00a019(7), 778 (1972)","journal-title":"Notices of the Am. Math. Soc."},{"key":"17_CR12","unstructured":"Rittri, M.: Searching program libraries by type and proving compiler correctness by bisimulation. PhD thesis, University of G\u00f6teborg, G\u00f6teborg, Sweden (1990)"},{"key":"17_CR13","volume-title":"Theory of Recursive Functions and Effective Computability","author":"H. Rogers Jr.","year":"1988","unstructured":"Rogers Jr., H.: Theory of Recursive Functions and Effective Computability, 2nd edn. The MIT Press, Cambridge (1988)","edition":"2"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/3-540-56944-8_71","volume-title":"Logic Programming and Automated Reasoning","author":"S.V. Soloviev","year":"1993","unstructured":"Soloviev, S.V.: A complete axiom system for isomorphism of types in closed categories. In: Voronkov, A. (ed.) LPAR 1993. LNCS, vol.\u00a0698, pp. 360\u2013371. Springer, Heidelberg (1993)"},{"key":"17_CR15","unstructured":"Wilkie, A.J.: On exponentiation\u2014A solution to Tarski\u2019s high school algebra problem. Math. Inst. Oxford University (1981) (preprint)"},{"key":"17_CR16","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1145\/604131.604146","volume-title":"Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"Y. Zibin","year":"2003","unstructured":"Zibin, Y., Gil, J., Considine, J.: Efficient algorithms for isomorphisms of simple types. In: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 160\u2013171. ACM Press, New York (2003)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32275-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T21:26:54Z","timestamp":1553290014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}