University of Illinois Urbana-Champaign

Circular Coinduction: A Proof Theoretical Foundation

Rosu, Grigore; Lucanu, Dorel

Content Files
UIUCDCS-R-2009-3037.pdf

Permalink

https://hdl.handle.net/2142/10840

Description

Title
Circular Coinduction: A Proof Theoretical Foundation
Author(s)
  • Rosu, Grigore
  • Lucanu, Dorel
Issue Date
2009-02
Keyword(s)
Computer Science
Date of Ingest
2009-04-15T14:44:24Z
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/10840

Owning Collections

Research and Tech Reports - Computer Science PRIMARY