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 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.

翻译：推断系统是一个广泛的框架,用来通过推断规则来界定可能重复的上游,它们允许相当仔细地研究进化和巧妙的诠释。在本文中,我们考虑一种中间方式的解释,称为定期解释,它结合了两种方法的优点:它允许非有充分根据的推理,同时又是有限的。我们表明,基于正常树木的正常解释的自然证据理论定义与一个合理的固定点相吻合。然后,我们提供了一种相当的感化定性,它导致一种算法,以寻找定期得出判断的算法。我们根据这些结果,界定了定期推理的证据技术:常规的硬化原则,以证明完整性,以及一种根据正常解释的内含性定性证明健全性的方法。最后,我们表明,常规方法可以顺利地延伸至带有共同规则的推断系统,即最近引入的概括性框架,允许人们改进硬体解释;证明,这种灵活的定期解释也承认了一种等同的自导性特征。