CycleQ: an efficient basis for cyclic equational reasoning
CycleQ: an efficient basis for cyclic equational reasoning
复制标题
CycleQ：循环方程推理的有效基础
DOI：
10.1145/3519939.3523731
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Jones E
中科院分区：
文献类型：
--
作者：
Jones E
我们提出了一个新的循环证明系统，用于纯函数程序行为的自动等式推理。该系统的关键是循环证明和式推理的方式是通过使用上下文替代作为切割规则来调解的。我们表明，我们的系统虽然简单，但已经包含了几种隐式归纳法的方法，这些方法被称为“无归纳法”、“重写归纳法”和“一致性证明法”。通过限制轨迹的形式，我们证明了我们的系统中的全局正确性可以增量验证，利用众所周知的大小变化原理，从而有效地实现了证明搜索。我们的CycleQ工具，作为一个GHC插件实现，在许多标准基准测试中显示出有希望的结果。
We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proofs and equational reasoning are mediated by the use of contextual substitution as a cut rule. We show that our system, although simple, already subsumes several of the approaches to implicit induction variously known as “inductionless induction”, “rewriting induction”, and “proof by consistency”. By restricting the form of the traces, we show that global correctness in our system can be verified incrementally, taking advantage of the well-known size-change principle, which leads to an efficient implementation of proof search. Our CycleQ tool, implemented as a GHC plugin, shows promising results on a number of standard benchmarks.
登录
查看更多内容
SMT 求解器的归纳
DOI：
--
发表时间：
2015
期刊：
International Conference on Verification, Model Checking and Abstract Interpretation
影响因子：
--
作者：
Andrew Reynolds;Viktor Kunčak
通讯作者：
Viktor Kunčak
DOI：
10.1007/978-3-642-45221-5_9
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Benzmüller C
通讯作者：
Benzmüller C
使用显式计划来指导归纳证明
DOI：
--
发表时间：
1988
期刊：
CADE
影响因子：
--
作者：
A. Bundy
通讯作者：
A. Bundy
DOI：
10.1016/s0747-7171(89)80069-0
发表时间：
1986
期刊：
J. Symb. Comput.
影响因子：
--
作者：
L. Fribourg
通讯作者：
L. Fribourg
无需构造函数的理论归纳自动证明
DOI：
10.1016/0890-5401(89)90062-x
发表时间：
1989
期刊：
Inf. Comput.
影响因子：
--
作者：
J. Jouannaud;Emmanuel Kounalis
通讯作者：
Emmanuel Kounalis