{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T18:08:46Z","timestamp":1726250926921},"publisher-location":"Berlin\/Heidelberg","reference-count":38,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540579354"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0032399","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:30:32Z","timestamp":1134282632000},"page":"133-172","source":"Crossref","is-referenced-by-count":11,"title":["Well-ordering of algebras and Kruskal's theorem"],"prefix":"10.1007","author":[{"given":"Ryu","family":"Hasegawa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/BF01175640","volume":"53","author":"W. Ackermann","year":"1951","unstructured":"W. Ackermann, Konstruktiver Aufbau eines Abschnitts der zweiten Cantorschen Zahlenklasse, Math. Z. 53 (1951) 403\u2013413.","journal-title":"Math. Z."},{"key":"9_CR2","series-title":"Lecture Notes in Mathematics 500","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/BFb0079544","volume-title":"Proof Theory Symposion","author":"W. Buchholz","year":"1975","unstructured":"W. Buchholz, Normalfunktionen und konstruktive Systeme von Ordinalzahlen, in: Proof Theory Symposion, Kiel 1974, J. Miller, G. H. M\u00fcller eds., Lecture Notes in Mathematics 500, (Springer, 1975) pp.4\u201325."},{"key":"9_CR3","unstructured":"W. Buchholz and K. Sch\u00fctte, Proof Theory of Impredicative Subsystems of Analysis, (Bibliopolis, 1988)."},{"key":"9_CR4","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1017\/S0022481200031224","volume":"51","author":"A. Cantini","year":"1986","unstructured":"A. Cantini, On the relation between choice and comprehension principles in second order arithmetic, J. Symb. Logic 51 (1986) 360\u2013373.","journal-title":"J. Symb. Logic"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"P. M. Cohn, Universal Algebra, Revised edition, (D. Reidel, 1981).","DOI":"10.1007\/978-94-009-8399-1"},{"key":"9_CR6","volume-title":"A proof of Higman's lemma by structural induction, manuscript","author":"T. Coquand","year":"1993","unstructured":"T. Coquand, A proof of Higman's lemma by structural induction, manuscript, April 1993, Chalmers University, G\u00f6teborg, Sweden, 4 pages."},{"key":"9_CR7","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/1385-7258(77)90067-1","volume":"39","author":"D. H. J. Jongh de","year":"1977","unstructured":"D. H. J. de Jongh and R. Parikh, Well-partial orderings and hierarchies, Indag. Math. 39 (1977) 195\u2013207.","journal-title":"Indag. Math."},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science 17 (1982) 279\u2013301.","journal-title":"Theoretical Computer Science"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science 668","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/3-540-56610-4_68","volume-title":"TAPSOFT '93: Theory and Practice of Software Development","author":"N. Dershowitz","year":"1993","unstructured":"N. Dershowitz, Trees, ordinals and termination, in: TAPSOFT '93: Theory and Practice of Software Development, Orsay, France, 1993, M.-C. Gaudel, J.-P. Jouannaud eds., Lecture Notes in Computer Science 668 (Springer, 1993) pp. 243\u2013250."},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and Z. Manna, Proving termination with multiset orderings, Comm. ACM (1979) 465\u2013476.","DOI":"10.1145\/359138.359142"},{"key":"9_CR11","first-page":"104","volume-title":"Proof theoretic techniques for term rewriting theory","author":"N. Dershowitz","year":"1988","unstructured":"N. Dershowitz and M. Okada, Proof theoretic techniques for term rewriting theory, in: Third Annual Symposium on Logic in Computer Science, July 1988, Edinburgh, Scotland, (IEEE, 1988) pp.104\u2013111."},{"key":"9_CR12","unstructured":"S. Feferman, Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, in: Intuitionism and Proof Theory, Proceedings of the Summer Conference at Buffalo N.Y. 1968, A, Kino, J. Myhill, R. E. Vesley eds., (North-Holland 1970) pp. 303\u2013326."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"S. Feferman, Preface: how we get from there to here, in: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, Lecture Notes in Mathematics 897 (Springer, 1981) pp.1\u201315.","DOI":"10.1007\/BFb0091895"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"H. Friedman, N. Robertson and P. Seymour, The metamathematics of the graph minor theorem, in: Contemporary Mathematics, Vol. 65, Logic and Combinatorics, Aug 1985, (AMS, 1987) pp.229\u2013261.","DOI":"10.1090\/conm\/065\/891251"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"H. Friedman, K. McAloon and S. Simpson, A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis, in: Patras Logic Symposion, G. Metakides ed., (North-Holland, 1982) pp. 197\u2013230.","DOI":"10.1016\/S0049-237X(08)71365-X"},{"key":"9_CR16","unstructured":"L. Fuchs, Partially Ordered Algebraic Systems, (Pengamon Press, 1963)."},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0168-0072(91)90022-E","volume":"53","author":"J. H. Gallier","year":"1991","unstructured":"J. H. Gallier, What's so special about Kruskal's theorem and the ordinal \u0393 0? A survey of some results in proof theory, Ann. Pure Appl Logic 53 (1991) 199\u2013260.","journal-title":"Ann. Pure Appl Logic"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BF01360719","volume":"174","author":"H. Gerber","year":"1967","unstructured":"H. Gerber, An extension of Sch\u00fctte's klammersymbols, Math. Ann. 174 (1967) 203\u2013216.","journal-title":"Math. Ann."},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science 620","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/BFb0023872","volume-title":"Logical Foundations of Computer Science \u2014 Tver '92","author":"A. Gupta","year":"1992","unstructured":"A. Gupta, A constructive proof that tree are well-quasi-ordered under minors (detailed abstract), in: Logical Foundations of Computer Science \u2014 Tver '92, A. Nerode, M. Taitslin eds., Tver, Russia, July 1992, Lecture Notes in Computer Science 620, (Springer, 1992) pp. 174\u2013185."},{"key":"9_CR20","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Higman","year":"1952","unstructured":"G. Higman, Ordering by divisibility in abstract algebras, Proc. London. Math. Soc. Third Series 2 (1952) 326\u2013336.","journal-title":"Proc. London. Math. Soc. Third Series"},{"key":"9_CR21","unstructured":"J.-P. Jouannaud and M. Okada, Satisfiability of systems of ordinal notations with the subterm property is decidable, preprint."},{"key":"9_CR22","unstructured":"S. Kamin and J.-J. L\u00e9vy, Attempts for generalizing the recursive path orderings, handwritten notes, Feb. 1980, 26pp."},{"key":"9_CR23","first-page":"210","volume":"95","author":"J. B. Kruskal","year":"1960","unstructured":"J. B. Kruskal, Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture, Trans. Am. Math. Soc. 95 (1960) 210\u2013225.","journal-title":"Trans. Am. Math. Soc."},{"key":"9_CR24","unstructured":"P. Lescanne, Two implementations of the recursive path ordering on monadic terms, Proc. 19th Allerton House Conference on Communication, Control and Computing, (University of Illinois Press, 1981) pp. 634\u2013643."},{"key":"9_CR25","first-page":"181","volume-title":"Uniform termination of term rewriting systems, recursive decomposition ordering with status","author":"P. Lescanne","year":"1984","unstructured":"P. Lescanne, Uniform termination of term rewriting systems, recursive decomposition ordering with status, in: Ninth Colloquium on Trees in Algebra and Programming, March 1984, Bordeaux, France, B. Courcelle ed., (Cambridge University Press, 1984) pp. 181\u2013194."},{"key":"9_CR26","first-page":"356","volume-title":"The order types of termination orderings on monadic terms, strings and multisets","author":"U. Martin","year":"1993","unstructured":"U. Martin and E. Scott, The order types of termination orderings on monadic terms, strings and multisets, Proc. Eighth Annual IEEE Symposium on Logic in Computer Science, June 1992 Montreal, Canada, (IEEE, 1993) pp. 356\u2013363."},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"C. R. Murthy and J. R. Russell, A constructive proof of Higman's lemma, in: Proceedings of the Fifth Annual Symposium on Logic in Computer Science, (IEEE, 1990) pp. 257\u2013267.","DOI":"10.1109\/LICS.1990.113752"},{"key":"9_CR28","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1017\/S0305004100003844","volume":"59","author":"C. S. J. A. Nash-Williams","year":"1963","unstructured":"C. St. J. A. Nash-Williams, On well-quasi-ordering finite trees, Proc. Camb. Philos. Soc. 59 (1963) 833\u2013835.","journal-title":"Proc. Camb. Philos. Soc."},{"key":"9_CR29","unstructured":"M. Okada and A. Steele, Ordering structures and the Knuth-Bendix completion algorithm, in: Proceedings of the Allerton Conference on Communication, Control and Computing, Monticello, IL, 1988."},{"key":"9_CR30","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0168-0072(93)90192-G","volume":"60","author":"M. Rathjen","year":"1993","unstructured":"M. Rathjen and A. Weiermann, Proof-theoretic investigations on Kruskal's theorem, Ann. Pure Appl. Logic 60 (1993) 49\u201388.","journal-title":"Ann. Pure Appl. Logic"},{"key":"9_CR31","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1006\/aima.1993.1004","volume":"97","author":"F. Richman","year":"1993","unstructured":"F. Richman and G. Stolzenberg, Well-quasi-ordered sets, Adv. Math 97 (1993) 145\u2013153.","journal-title":"Adv. Math"},{"key":"9_CR32","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0095-8956(90)90120-O","volume":"48","author":"N. Robertson","year":"1990","unstructured":"N. Robertson and P. D. Seymour, Graph minors IV. Tree-width and well-quasi-ordering, J. Comb. Th. Series B 48 (1990) 227\u2013254.","journal-title":"J. Comb. Th. Series B"},{"key":"9_CR33","unstructured":"K. Sakai, Knuth-Bendix algorithm for Thue system based on kachinuki ordering, ICOT Technical Memorandum: TM-0087, ICOT, Institute for New Generation Computer Technology, Dec. 1984"},{"key":"9_CR34","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BF02007558","volume":"25","author":"K. Sch\u00fctte","year":"1985","unstructured":"K. Sch\u00fctte and S. G. Simpson, Ein in der reinen Zahlentheorie unbeweisbarer Satz \u00fcber endliche Folgen von nat\u00fcrlichen Zahlen, Arch. Math. Logik Grundlagenforsch 25 (1985) 75\u201389.","journal-title":"Arch. Math. Logik Grundlagenforsch"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"S. G. Simpson, Reverse mathematics, in: Recursion Theory, A. Nerode, R. A. Shore, eds., Proceedings of Symposia in Pure Mathematics, Volume 42 (AMS, 1985) pp. 461\u2013471.","DOI":"10.1090\/pspum\/042\/791071"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"S. G. Simpson, Nonprovability of certain combinatorial properties of finite trees, in: Harvey Friedman's research on the foundations of mathematics, L. A. Harrington, M. D. Morley, A. Scedrov, S. G. Simpson, eds., (North-Holland, 1985) pp. 87\u2013117.","DOI":"10.1016\/S0049-237X(09)70156-9"},{"key":"9_CR37","doi-asserted-by":"crossref","first-page":"961","DOI":"10.2307\/2274585","volume":"53","author":"S. G. Simpson","year":"1988","unstructured":"S. G. Simpson, Ordinal numbers and the Hilbert basis theorem, J. Symbolic Logic 53 (1988) 961\u2013974.","journal-title":"J. Symbolic Logic"},{"key":"9_CR38","first-page":"213","volume":"5","author":"K. Tanaka","year":"1992","unstructured":"K. Tanaka, Reverse mathematics and subsystems of second-order arithmetic, Sugaku Expositions 5 (1992) 213\u2013234.","journal-title":"Sugaku Expositions"}],"container-title":["Lecture Notes in Computer Science","Logic, Language and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0032399","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:47:33Z","timestamp":1586612853000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0032399"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540579354"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/bfb0032399","relation":{},"subject":[]}}