22023-04-01 06:35:02DanielaZaharie12023-04-01 06:34:36DanielaZaharieMechanical Certification of FOLID Cyclic Proofs Sorin Stratulat, University of Lorraine, France Abstract Cyclic induction is a powerful reasoning technique that can soundly stop the proof development and make the proof experience successful. In the setting of first-order logic with inductive definitions (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, as Isabelle and Coq. We propose a solution to check in Coq the cyclic proofs produced by E-Cyclist, an extension of Cyclist that implements a more efficient soundness validation method, by using the very general Noetherian induction principle integrated in Coq. Our work is based on a methodology already used successfully for certifying formula-based Noetherian induction proofs.