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

Sorin Stratulat
(Université de Lorraine, CNRS, LORIA)

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.

In Temur Kutsia: Proceedings of the 9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), Hagenberg, Austria, September 8-10, 2021, Electronic Proceedings in Theoretical Computer Science 342, pp. 129–135.
Published: 6th September 2021.

ArXived at: http://dx.doi.org/10.4204/EPTCS.342.11 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org