E-Cyclist: Implementation of an Efficient Validation of FOL ID Cyclic Induction Reasoning (System Description)

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 ordering measures that satisfy the ordering constraints. FOLID cyclic proof derivations may also be hard to certify. E-Cyclist witnesses a strong relation between the two cyclic and well-founded induction reasonings. This opens the perspective of using the known certification methods that work for well-founded induction proofs.

Domaines: Calcul formel [cs.SC]

Sorin Stratulat. E-Cyclist: Implementation of an Efficient Validation of FOL ID Cyclic Induction Reasoning (System Description). 2020. ⟨hal-02464242v1⟩