关于拟序图系统
On Quasi Ordinal Diagram Systems
摘要：
本文的目的有两个：首先，我们推广Okada-Takeuti的良好拟序图理论，利用最近的结果Dershowitz-Tzameret的版本的树嵌入定理与间隙条件。其次，我们讨论了可能使用这样的强序数符号系统的目的，一个典型的传统的终止证明方法长期重写系统，特别是二阶（基于模式匹配）重写系统，包括重写理论版本的布赫霍尔茨的九头蛇游戏。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
