E-Cyclist：FOLID 循环归纳推理高效验证的实现
计算机科学中的逻辑
2021-09-09 v1
摘要
带归纳定义的一阶逻辑（FOLID）循环归纳推理的可靠性检查是可判定的，但标准检查方法基于 Böchi 自动机的指数级补运算。近来，我们提出了一种多项式级检查方法，其最昂贵的步骤类似于使用多集路径序进行比较。我们描述了该方法在 Cyclist 证明器中的实现。称为 E-Cyclist 的它成功检查了 Cyclist 原始发行版中包含的所有证明。我们设计了启发式方法，通过对证明推导的分析自动定义基于迹的序度量，以保证可靠性性质。
引用
@article{arxiv.2109.03235,
title = {E-Cyclist: Implementation of an Efficient Validation of FOLID Cyclic Induction Reasoning},
author = {Sorin Stratulat},
journal= {arXiv preprint arXiv:2109.03235},
year = {2021}
}
备注
In Proceedings SCSS 2021, arXiv:2109.02501