查看文章

Checking the soundness of the cyclic induction reasoning for first-order logic with in-ductive definitions (FOL_ID) is decidable but the standard checking method is based on a doubly exponential complement operation for Büchi automata. We present a polynomial method 'semi-deciding' this problem; its most expensive steps recall the comparisons with multiset path orderings. In practice, it has been integrated in the Cyclist prover and successfully checked all the proofs included in its distribution. FOL_ID cyclic proofs may also be hard to certify. Our method helps to represent the cyclic induction reasoning as being well-founded, where the ordering constraints are automatically built from the analysis of the proofs. Hence, it creates a bridge between the two induction reasoning methods and opens the perspective to use the certification methods adapted for well-founded induction proofs. Introduction. Cyclic pre-proofs for the classical first-order logic with inductive predicates (FOL_ID) have been extensively studied in [1, 2, 4]. They are finite sequent-based derivations where some terminal nodes, called buds, are labelled with sequents already occurring in the derivation, called companions. Bud-companion (BC) relations, graphically represented as back-links, are described by an induction function attached to the derivation, such that only one companion is assigned to each bud, but a node can be the companion of one or several buds. The pre-proofs can be viewed as digraphs whose cycles, if any, are introduced by the BC-relations. It is easy to build unsound pre-proofs, for example by creating a BC-relation between the nodes labelled by the …