Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

ENTCS

2007

2007

This paper is concerned with a proof-theoretic observation about two kinds of proof systems for regular cyclic objects. It is presented for the case of two formal systems that are complete with respect to the notion of “recursive type equality” on a restricted class of recursive types in µ-term notation. Here we show the existence of an immediate duality with a geometrical visualization between proofs in a variant of the coinductive axiom system due to Brandt and Henglein and “consistency-unfoldings” in a variant of a ‘syntacticmatching’ proof system for testing equations between recursive types due to Ariola and Klop. Finally we sketch an analogous result of a duality between a similar pair of proof systems for bisimulation equivalence on equational speciﬁcations of cyclic term graphs.

Added |
13 Dec 2010 |

Updated |
13 Dec 2010 |

Type |
Journal |

Year |
2007 |

Where |
ENTCS |

Authors |
Clemens Grabmayer |

Comments (0)