一句话：为推理系统提出正则解释，统一归纳与余归纳，建立证明论与算法基础，并扩展到 corules。
推理系统用推理规则定义可能递归的谓词，已有归纳与余归纳两种解释。本文研究介于二者之间的 regular 解释：它允许非良基推理，同时保持有限性。作者首先证明基于 regular trees 的自然证明论定义与 rational fixed point 重合，随后给出等价的归纳刻画，并据此设计寻找 judgment 的 regular derivation 的算法。基于这些结果，论文提出 regular coinduction principle 用于证明完备性，以及基于归纳刻画的归纳技术用于证明可靠性。最后，作者将 regular 方法扩展到带 corules 的推理系统，证明这一更灵活的解释同样具有等价的归纳刻画。
Inference systems are a widespread framework used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. In this paper, we consider a middle way interpretation, called regular, which combines advantages of both approaches: it allows non-well-founded reasoning while being finite. We show that the natural proof-theoretic definition of the regular interpretation, based on regular trees, coincides with a rational fixed point. Then, we provide an equivalent inductive characterization, which leads to an algorithm which looks for a regular derivation of a judgment. Relying on these results, we define proof techniques for regular reasoning: the regular coinduction principle, to prove completeness, and an inductive technique to prove soundness, based on the inductive characterization of the regular interpretation. Finally, we show the regular approach can be smoothly extended to inference systems with corules, a recently introduced, generalised framework, which allows one to refine the coinductive interpretation, proving that also this flexible regular interpretation admits an equivalent inductive characterisation.