正常共归纳的基础
摘要：正规推理：定义可能通过推理规则来定义可能递归谓词的广泛框架。它们允许归纳和协同解释，并且已经有相当多的研究。在本文中，我们考虑了一种中间方式的解释，称为正规解释，它结合了两种方法的优点：它允许非良好基础的推理，同时又是有限的。我们证明了正规解释的自然证明论定义，基于正规树，与一个有理不动点相一致。然后，我们提供了一个等价的归纳特征，这导致了一种寻找判断的正规推导的算法。依靠这些结果，我们定义了正规推理的证明技巧：正规协同递归原则，用于证明完备性，以及基于正规解释的归纳特征的归纳技巧，用于证明一致性。最后，我们展示了正规方法如何平滑地扩展到具有共规则的推理系统，这是一个最近引入的广义框架，可以细化协同解释。证明了这个灵活的正规解释也具有等价的归纳特征。
作者：Francesco Dagnino
论文ID：2006.02887
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22