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.

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