A duality between proof systems for cyclic term graphs

C.A. Grabmayer

Research output: Contribution to JournalArticleAcademicpeer-review

194 Downloads (Pure)


This paper presents a proof-theoretic observation about two kinds of proof systems for bisimilarity between cyclic term graphs. First we consider proof systems for demonstrating that term specifications of cyclic term graphs have the same tree unwinding. We establish a close connection between adaptations for terms over a general first-order signature of the coinductive axiomatisation of recursive type equivalence by Brandt and Henglein (Brandt and Henglein 1998) and of a proof system by Ariola and Klop (Ariola and Klop 1995) for consistency checking. We show that there exists a simple duality by mirroring between derivations in the former system and formalised consistency checks, which are called consistency unfoldings', in the latter. This result sheds additional light on the axiomatisation of Brandt and Henglein: it provides an alternative soundness proof for the adaptation considered here. We then outline an analogous duality result that holds for a pair of similar proof systems for proving that equational specifications of cyclic term graphs are bisimilar. © 2007 Cambridge University Press.
Original languageEnglish
Pages (from-to)439-484
JournalMathematical Structures in Computer Science (MSCS)
Issue number3
Publication statusPublished - 2007

Bibliographical note



Dive into the research topics of 'A duality between proof systems for cyclic term graphs'. Together they form a unique fingerprint.

Cite this