Building explicit induction schemas for cyclic induction reasoning

ABSTRACT. In the setting of classical first-order logic with inductive predicates, two kinds of sequent-based induction reasoning are distinguished: cyclic and structural. Proving their equivalence is of great theoretical and practical interest for the automated reasoning community. It has been shown previously how to transform structural proofs developed with the LKID system into cyclic proofs using the CLKID$^\omega$ system. However, the inverse transformation was only conjectured.

We provide a simple procedure that performs the inverse transformation for an extension of LKID with explicit induction rules issued from the structural analysis of CLKID$^{\omega}$ proofs, then establish the equivalence of the two systems. This result is further refined for an extension of LKID with Noetherian induction rules. Based on it, we propose a solution for validating cyclic reasoning by (higher-order) sequent-based systems integrating the Noetherian induction principle, like Coq.