Iterative Circular Coinduction for CoCasl in Isabelle/HOL
Iterative Circular Coinduction for CoCasl in Isabelle/HOL
复制标题
Isabelle/HOL 中 CoCasl 的迭代循环共导
DOI：
10.1007/978-3-540-31984-9_26
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Lutz Schroder
中科院分区：
文献类型：
--
作者：
Daniel Hausmann;Till Mossakowski;Lutz Schroder
近年来，协代数已被公认为在适当的一般性水平上处理反应系统的选择框架。关于共代数系统反应性的证明通常依赖于共归纳法。与需要发明双模拟关系的“传统”共感应相比，圆形共感应方法允许更高程度的自动化。作为对代数-共代数规范语言的证明支持的一部分，我们开发了一种新的协归纳证明策略，该策略迭代地构建了一个双模拟关系，从而得到了循环协归纳的一个新变体。基于这一结果，我们为定理证明者Isabelle设计并实现了允许自动和半自动共归纳证明的策略。这种方法的灵活性是通过cocasl规范的（半）自动证明结果的例子来证明的，cocasl规范通过不莱梅异构casl工具集Hets自动转化为Isabelle理论。
Coalgebra has in recent years been recognized as the framework of choice for the treatment of reactive systems at an appropriate level of generality. Proofs about the reactive behavior of a coalgebraic system typically rely on the method of coinduction. In comparison to ‘traditional’ coinduction, which has the disadvantage of requiring the invention of a bisimulation relation, the method ofcircular coinductionallows a higher degree of automation. As part of an effort to provide proof support for the algebraic-coalgebraic specification languageCoCasl, we develop a new coinductive proof strategy which iteratively constructs a bisimulation relation, thus arriving at a new variant of circular coinduction. Based on this result, we design and implement tactics for the theorem prover Isabelle which allow for both automatic and semiautomatic coinductive proofs. The flexibility of this approach is demonstrated by means of examples of (semi-)automatic proofs of consequences ofCoCaslspecifications, automatically translated into Isabelle theories by means of the Bremen heterogeneousCasltool set Hets.
登录
查看更多内容
使用泛化批评来寻找共归纳证明的互模拟
DOI：
--
发表时间：
1997
期刊：
CADE
影响因子：
--
作者：
Louise Dennis;A. Bundy;I. Green
通讯作者：
I. Green
DOI：
--
发表时间：
2002
期刊：
Workshop on Recent Trends in Algebraic Development Techniques
影响因子：
--
作者：
J. Goguen;Kai Lin;Grigore Roşu
通讯作者：
Grigore Roşu
DOI：
10.1007/978-3-540-40020-2_21
发表时间：
2002
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
Till Mossakowski
通讯作者：
Till Mossakowski
CoCasl 中的代数-代数规范
DOI：
10.1016/j.jlap.2005.09.006
发表时间：
2003
期刊：
J. Log. Algebraic Methods Program.
影响因子：
--
作者：
Till Mossakowski;Horst Reichel;Markus Roggenbach;Lutz Schröder
通讯作者：
Lutz Schröder
自动推导—CADE-14
影响因子：
5
作者：
W. McCune
通讯作者：
W. McCune