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

TL;DR

The paper presents E-Cyclist, an efficient implementation for validating cyclic induction reasoning in FOLID, using a polynomial-time method integrated into the Cyclist prover, with heuristics for automatic measure selection.

Contribution

It introduces a novel polynomial-time validation method for FOLID cyclic reasoning and its implementation in the Cyclist prover, improving efficiency over traditional exponential approaches.

Findings

Successfully checked all proofs in Cyclist distribution

Implemented heuristics for automatic measure selection

Demonstrated efficiency of the polynomial checking method

Abstract

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\"uchi 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.