一句话：提出统一的余归纳框架，用于定义并推理无穷重写与无穷等式逻辑，无需序数或度量收敛。
论文关注无穷重写与无穷等式逻辑的基础问题：如何以统一方式定义并推理任意长度甚至超限序数长度的重写序列与等式推导，同时避免引入序数或度量收敛等复杂结构。作者提出一个余归纳框架，将无穷等式逻辑和项重写视为余归纳定义的对象，并用余归纳证明原则进行推理。该框架能刻画任意序数长度的重写序列，却不需要显式序数，也不依赖度量收敛，因而特别适合在定理证明助手中形式化。摘要未给出具体定理或基准评估，主要贡献是概念框架与统一基础。
We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.Comment: arXiv admin note: substantial text overlap with arXiv:1505.01128, arXiv:1306.6224
@article{paperbot439,
title = {Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic},
author = {Jörg Endrullis and Helle Hvid Hansen and Dimitri Hendriks and Andrew Polonsky and Alexandra Silva},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:3)2018}
}