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

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 expen...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2021-09
Main Author: Stratulat, Sorin
Format: Article
Language:English
Subjects:
Polynomials
Reasoning
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422
DOI:10.48550/arxiv.2109.03235