E-Cyclist: Implementation of an Efficient Validation of FOL ID Cyclic Induction Reasoning

Sorin Stratulat (1)

1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems

Checking the soundness of cyclic induction reasoning for first-order logic with inductive definitions (FOLID) is decidable but the standard checking method is based on an exponential complement operation for Büchi automata. Recently, we introduced a polynomial checking method whose most expensive steps recall the comparisons done with multiset path orderings. We describe the implementation of our method in the Cyclist prover. Referred to as E-Cyclist, it successfully checked all the proofs included in the original distribution of Cyclist. Heuristics have been devised to automatically define, from the analysis of the proof derivations, the trace-based ordering measures that guarantee the soundness property.

Domaines: Calcul formel [cs.SC]

Sorin Stratulat. E-Cyclist: Implementation of an Efficient Validation of FOL ID Cyclic Induction Reasoning. SCSS 2021 - 9th International Symposium on Symbolic Computation in Software Science, Sep 2021, Linz, Austria. pp.129--135. ⟨hal-02464242v4⟩