查看文章

Cyclic induction is a powerful reasoning technique that consists in blocking the proof development of certain subgoals already encountered during the proof process. In the setting of first-order logic with inductive definitions and equality (FOL_ID), cyclic proofs can be built automatically by the Cyclist prover, but their implementations are error-prone and the human validation may be tedious. On the other hand, cyclic induction is not yet integrated into certifying proof environments that support first-order logic and inductive definitions, such as Isabelle and Coq. We propose a solution to check, using Coq, the cyclic proofs produced by E-Cyclist, an extension of Cyclist that implements a more efficient soundness validation method, by using the general Noetherian induction principle integrated into Coq. Our work is based on a methodology for certifying first-order formula-based Noetherian induction proofs, such as those …