{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,12]],"date-time":"2022-08-12T02:28:06Z","timestamp":1660271286199},"reference-count":17,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:00:00Z","timestamp":1180656000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2007,6]]},"abstract":"<jats:p>This paper presents a proof-theoretic observation about two kinds of proof systems for bisimilarity between cyclic term graphs.<\/jats:p><jats:p>First we consider proof systems for demonstrating that \u03bc term specifications of cyclic term graphs have the same tree unwinding. We establish a close connection between adaptations for \u03bc 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 \u2018consistency 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.<\/jats:p><jats:p>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.<\/jats:p>","DOI":"10.1017\/s0960129507006111","type":"journal-article","created":{"date-parts":[[2007,7,6]],"date-time":"2007-07-06T13:51:23Z","timestamp":1183729883000},"page":"439-484","source":"Crossref","is-referenced-by-count":2,"title":["A duality between proof systems for cyclic term graphs"],"prefix":"10.1017","volume":"17","author":[{"given":"CLEMENS","family":"GRABMAYER","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,6,1]]},"reference":[{"key":"S0960129507006111_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"S0960129507006111_ref14","unstructured":"Rosu G. and Goguen J. (2001) Circular coinduction. In: Proceedings of IJCAR'01, Siena, Italy."},{"key":"S0960129507006111_ref10","first-page":"376","volume-title":"Proceedings of LICS'91","author":"H\u00fcttel","year":"1991"},{"key":"S0960129507006111_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/321312.321326"},{"key":"S0960129507006111_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717"},{"key":"S0960129507006111_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90023-0"},{"key":"S0960129507006111_ref2","unstructured":"Ariola Z. M. and Klop J. W. (1995) Equational term graph rewriting. Technical Report IR-391, Vrije Universiteit Amsterdam. (This is an extension of Ariola and Klop (1996).)"},{"key":"S0960129507006111_ref8","unstructured":"Grabmayer C. (2005) Relating Proof Systems for Recursive Types, Ph.D. thesis, Vrije Universiteit Amsterdam."},{"key":"S0960129507006111_ref4","unstructured":"Blom S. (2001) Term Graph Rewriting, Syntax and Sematics, Ph.D. thesis, Vrije Universiteit Amsterdam."},{"key":"S0960129507006111_ref7","unstructured":"Grabmayer C. (2002b) A duality in proof systems for recursive type equality and bisimulation equivalence on cyclic term graphs. Technical Report IR-499, Dept. of Math. and Comp. Sci., Vrije Universiteit Amsterdam. (Available from the authors's home page.)"},{"key":"S0960129507006111_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"S0960129507006111_ref3","doi-asserted-by":"crossref","first-page":"207","DOI":"10.3233\/FI-1996-263401","article-title":"Equational term graph rewriting","volume":"26","author":"Ariola","year":"1996","journal-title":"Fundamenta Informaticae"},{"key":"S0960129507006111_ref5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FI-1998-33401","article-title":"Coinductive axiomatization of recursive type equality and subtyping","volume":"33","author":"Brandt","year":"1998","journal-title":"Fundamenta Informaticae"},{"key":"S0960129507006111_ref6","doi-asserted-by":"crossref","unstructured":"Grabmayer C. (2002a) A duality in proof systems for recursive type equality and bisimulation equivalence on cyclic term graphs. In: Plump D. (ed.) Proceedings of TERMGRAPH 2002. Electronic Notes in Computer Science 72 (1).","DOI":"10.1016\/j.entcs.2002.09.007"},{"key":"S0960129507006111_ref9","doi-asserted-by":"publisher","DOI":"10.2307\/2586843"},{"key":"S0960129507006111_ref11","unstructured":"Klop J. W. (2000) Proof systems for cyclic term graphs. Lecture at the Winter Workshop on Logics, Types and Rewriting, February 1-3 2000, Heriot-Watt University, Edinburgh. (Available at: http:\/\/www.cs.vu.nl\/jwk\/ctg1-41.pdf.)"},{"key":"S0960129507006111_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00242-0"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129507006111","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,24]],"date-time":"2020-04-24T03:17:56Z","timestamp":1587698276000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129507006111\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,6]]}},"alternative-id":["S0960129507006111"],"URL":"https:\/\/doi.org\/10.1017\/s0960129507006111","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6]]}}}