A Generic Cyclic Theorem Prover
A Generic Cyclic Theorem Prover
复制标题
通用循环定理证明者
DOI：
10.1007/978-3-642-35182-2_25
复制
发表时间：
2012
影响因子：
0.6
通讯作者：
R. Petersen
中科院分区：
文献类型：
--
作者：
J. Brotherston;Nikos Gorogiannis;R. Petersen
我们描述了一个自动定理供体的设计和实现，这些宣传师意识到了完全循环证明的一般概念。我们的工具称为\（\ textsc {骑自行车的人} \），能够构建证明，以遵守一个非常通用的周期方案，其中叶子可以将叶子链接到证明中的任何其他匹配节点，并验证一般的，全局的无限制条件这样的证明对象确保它们的声音。 \（\ textsc {骑自行车的人} \）基于一种新的循环证明理论，可以将其实例化为各种逻辑。我们基于以下方式开发了三个这样的具体实例，（a）具有归纳定义的一阶逻辑； （b）纯粹的分离逻辑的需要； （c）指针程序的Hoare式终止证明。实验进行的实验表明，\（\ textsc {cyclist} \）为归纳定理证明的未来平台提供了巨大的潜力。
We describe the design and implementation of an automated theorem prover realising a fully general notion of cyclic proof. Our tool, called \(\textsc{Cyclist}\), is able to construct proofs obeying a very general cycle scheme in which leaves may be linked to any other matching node in the proof, and to verify the general, global infinitary condition on such proof objects ensuring their soundness. \(\textsc{Cyclist}\) is based on a new, generic theory of cyclic proofs that can be instantiated to a wide variety of logics. We have developed three such concrete instantiations, based on: (a) first-order logic with inductive definitions; (b) entailments of pure separation logic; and (c) Hoare-style termination proofs for pointer programs. Experiments run on these instantiations indicate that \(\textsc{Cyclist}\) offers significant potential as a future platform for inductive theorem proving.
使用分析表和相关方法进行自动推理
DOI：
10.1007/978-3-642-40537-2_17
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Khodadadi M
通讯作者：
Khodadadi M