Mechanical 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.