CiRCULAR Coinduction: A proof theoretical foundation

Grigore Roşu, Dorel Lucanu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationAlgebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings
Pages127-144
Number of pages18
DOIs
StatePublished - 2009
Event3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009 - Udine, Italy
Duration: Sep 7 2009Sep 10 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5728 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009
CountryItaly
CityUdine
Period9/7/099/10/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'CiRCULAR Coinduction: A proof theoretical foundation'. Together they form a unique fingerprint.

Cite this