期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2019
卷号：288
页码：38-49
DOI：10.4204/EPTCS.288.4
语种：English
出版社：Open Publishing Association
摘要：The purposes of this note are the following two; we first generalize Okada-Takeuti's well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret's version of tree embedding theorem with gap conditions. Second, we discuss possible use of such strong ordinal notation systems for the purpose of a typical traditional termination proof method for term rewriting systems, especially for second-order (pattern-matching-based) rewriting systems including a rewrite-theoretic version of Buchholz's hydra game.
