TY - GEN
T1 - CiRCULAR Coinduction
T2 - 3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009
AU - Roşu, Grigore
AU - Lucanu, Dorel
N1 - Copyright:
Copyright 2009 Elsevier B.V., All rights reserved.
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70350352244&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70350352244&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-03741-2_10
DO - 10.1007/978-3-642-03741-2_10
M3 - Conference contribution
AN - SCOPUS:70350352244
SN - 3642037402
SN - 9783642037405
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 127
EP - 144
BT - Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings
Y2 - 7 September 2009 through 10 September 2009
ER -