CIRC : A Circular Coinductive Prover
CIRC : A Circular Coinductive Prover
复制标题
CIRC : 圆形感应证明器
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Grigore Roşu
中科院分区：
文献类型：
--
作者：
D. Lucanu;Grigore Roşu
CIRC是一个自动循环余感验证器，作为Maude的扩展而实现。讨论了构成CIRC核心的循环共感技术，以及使用元级重写逻辑能力的高级实现。为了反映CIRC在自动证明行为性质方面的优势，给出了一个定义和证明无限二叉树无穷流性质的例子。中国保监会还为自动归纳证明提供有限的支持，自动归纳证明可以与协归纳结合使用。
CIRC is an automated circular coinductive prover implemented as an extension of Maude. The circular coinductive technique that forms the core of CIRC is discussed, together with a high-level implementation using metalevel capabilities of rewriting logic. To reflect the strength of CIRC in automatically proving behavioral properties, an example defining and proving properties about infinite streams of infinite binary trees is shown. CIRC also provides limited support for automated inductive proving, which can be used in combination with coinduction.
Isabelle/HOL 中 CoCasl 的迭代循环共导
DOI：
10.1007/978-3-540-31984-9_26
发表时间：
2005
期刊：
影响因子：
--
作者：
Daniel Hausmann;Till Mossakowski;Lutz Schroder
通讯作者：
Lutz Schroder