Circular Coinduction: A Proof Theoretical Foundation

Rosu, Grigore; Lucanu, Dorel

Permalink

https://hdl.handle.net/2142/11524 Copy

Description

Title

Circular Coinduction: A Proof Theoretical Foundation

Author(s)

• Rosu, Grigore
• Lucanu, Dorel

Issue Date

2009-02

Keyword(s)

computer science

Abstract

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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11524

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections