Mechanical certification of FOLID cyclic proofs

International audienceCyclic 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 (FOLID), 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 in certifying proof environments that support first-order logic and inductive definitions, as Isabelle and Coq