Circular Coinduction: A Proof Theoretical Foundation
Circular Coinduction: A Proof Theoretical Foundation
复制标题
循环共导：证明理论基础
DOI：
10.1007/978-3-642-03741-2_10
复制
发表时间：
2009
影响因子：
0.6
通讯作者：
D. Lucanu
中科院分区：
文献类型：
--
作者：
Grigore Roşu;D. Lucanu
在过去的十年中，已经提出并实现了几种算法变体的循环coinduction，但证明理论基础的循环coinduction在其充分的一般性仍然缺失。本文给出了一个三规则证明系统，可用于形式推导循环共归纳证明。这三个规则系统被证明是行为上的声音，并证明了无限流的几个属性为例。循环共归纳的数学变体现在变成了使用这三条规则搜索证明推导的数学。
Several algorithmic variants of circular coinduction have been proposed and implemented during the last decade, but a proof theoretical foundation of circular coinduction in its full generality is still missing. This paper gives a three-rule proof system that can be used to formally derive circular coinductive proofs. This three-rule system is proved behaviorally sound and is exemplified by proving several properties of infinite streams. Algorithmic variants of circular coinduction now become heuristics to search for proof derivations using the three rules.
Isabelle/HOL 中 CoCasl 的迭代循环共导
DOI：
10.1007/978-3-540-31984-9_26
发表时间：
2005
期刊：
影响因子：
--
作者：
Daniel Hausmann;Till Mossakowski;Lutz Schroder
通讯作者：
Lutz Schroder