AI 中文总结
本文提出归约对字典序组合的简单判据，将其应用于多项式解释、矩阵解释等，研究矩阵解释的字典序变体，通过含Touzet的Hydra Battle的实验验证有效性。
AI 中文摘要
我们提出一种用于字典序组合归约对的简单判据，该判据适用于任意类别的归约对，例如多项式解释、矩阵解释和Knuth-Bendix序。此外，我们研究了矩阵解释的一种变体，其中采用字典序替代通常的分量序。通过包括Touzet的Hydra Battle在内的实验和示例验证了其有效性。
英文摘要
We present a simple criterion for combining reduction pairs lexicographically. The criterion is applicable to arbitrary classes of reduction pairs, such as the polynomial interpretation, the matrix interpretation, and the Knuth-Bendix order. In addition, we investigate a variant of the matrix interpretation where the lexicographic order is employed instead of the usual component-wise order. Effectiveness is demonstrated by experiments and examples, including Touzet's Hydra Battle.
