{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215251},"reference-count":30,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2007,10,1]],"date-time":"2007-10-01T00:00:00Z","timestamp":1191196800000},"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,10]]},"abstract":"<jats:p>Object-oriented (OO) programming techniques can be applied to equational specification logics by distinguishing <jats:italic>visible<\/jats:italic> data from <jats:italic>hidden<\/jats:italic> data (that is, by distinguishing the output of methods from the objects to which the methods apply), and then focusing on the behavioural equivalence of hidden data in the sense introduced by H. Reichel in 1984. Equational specification logics structured in this way are called <jats:italic>hidden equational logics<\/jats:italic>, HELs. The central problem is how to extend the specification of a given HEL to a specification of behavioural equivalence in a computationally effective way. S. Buss and G. Ro\u015fu showed in 2000 that this is not possible in general, but much work has been done on the partial specification of behavioural equivalence for a wide class of HELs. The OO connection suggests the use of coalgebraic methods, and J. Goguen and his collaborators have developed coinductive processes that depend on an appropriate choice of a <jats:italic>cobasis<\/jats:italic>, which is a special set of contexts that generates a subset of the behavioural equivalence relation. In this paper the theoretical aspects of coinduction are investigated, specifically its role as a supplement to standard equational logic for determining behavioural equivalence. Various forms of coinduction are explored. A simple characterisation is given of those HELs that are behaviourally specifiable. Those sets of conditional equations that constitute a complete, finite cobasis for a HEL are characterised in terms of the HEL's specification. Behavioural equivalence, in the form of logical equivalence, is also an important concept for single-sorted logics, for example, sentential logics such as the classical propositional logic. The paper is an application of the methods developed through the extensive work that has been done in this area on HELs, and to a broader class of logics that encompasses both sentential logics and HELs.<\/jats:p>","DOI":"10.1017\/s0960129507006305","type":"journal-article","created":{"date-parts":[[2007,10,4]],"date-time":"2007-10-04T04:46:43Z","timestamp":1191473203000},"page":"1075-1113","source":"Crossref","is-referenced-by-count":12,"title":["Behavioural reasoning for conditional equations"],"prefix":"10.1017","volume":"17","author":[{"given":"MANUEL A.","family":"MARTINS","sequence":"first","affiliation":[]},{"given":"DON","family":"PIGOZZI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,10,1]]},"reference":[{"key":"S0960129507006305_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-6942-2"},{"key":"S0960129507006305_ref27","unstructured":"Ro\u015fu G. (2000) Hidden logic, Ph.D. thesis, University of California, San Diego."},{"key":"S0960129507006305_ref25","first-page":"2","volume-title":"Encyclopedia of Mathematics","author":"Pigozzi","year":"2001"},{"key":"S0960129507006305_ref24","unstructured":"Martins M. (2004) Behavioral reasoning in generalized hidden logics, Ph.D. thesis, University of Lisbon."},{"key":"S0960129507006305_ref22","first-page":"123","volume-title":"Proceedings, Automated Software Engineering'00, Grenoble, France","author":"Lin","year":"2000"},{"key":"S0960129507006305_ref21","unstructured":"Leavens G. and Pigozzi D. (2002) Equational reasoning with subtypes, Iowa State University, Technical Report TR #02-07 (available at ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR02-07\/TR.pdf.)"},{"key":"S0960129507006305_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00068-0"},{"key":"S0960129507006305_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49253-4_20"},{"key":"S0960129507006305_ref18","unstructured":"Hennicker R. (1997) Structural specifications with behavioural operators: semantics, proof methods and applications, Habilitationsschrift Institut f\u00fcr Informatik, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"S0960129507006305_ref17","unstructured":"Gorbunov V. (1998) Algebraic theory of quasivarieties, (Siberian School of Algebra and Logic), Consultants Bureau, Plenum Publishing Corporation (translated from the Russian)."},{"key":"S0960129507006305_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40020-2_12"},{"key":"S0960129507006305_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00275-3"},{"key":"S0960129507006305_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129599002777"},{"key":"S0960129507006305_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69962-7"},{"key":"S0960129507006305_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"S0960129507006305_ref8","volume-title":"Coalgebraic Methods in Computer Science: CMCS 2000","author":"Buss","year":"2000"},{"key":"S0960129507006305_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00014-3"},{"key":"S0960129507006305_ref2","first-page":"41","volume-title":"Springer-Verlag Lecture Notes in Computer Science","author":"Bidoit","year":"1994"},{"key":"S0960129507006305_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00333-4"},{"key":"S0960129507006305_ref4","unstructured":"Bidoit M. and Hennicker R. (1999) Observer complete definitions are behaviourally coherent. In: Proc. OBJ\/CafeOBJ\/Maude Workshop at Formal Methods'99, Toulouse, France 83\u201394."},{"key":"S0960129507006305_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50325-0_3"},{"key":"S0960129507006305_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053582"},{"key":"S0960129507006305_ref10","first-page":"74","article-title":"Behavioural coherence in object-oriented algebraic specification","volume":"6","author":"Diaconescu","year":"2000","journal-title":"Journal of Universal Computer Science"},{"key":"S0960129507006305_ref6","first-page":"396","article-title":"Algebraizable logics","author":"Blok","year":"1989","journal-title":"Mem. Am. Math. Soc"},{"key":"S0960129507006305_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00039-4"},{"key":"S0960129507006305_ref9","doi-asserted-by":"crossref","unstructured":"Diaconescu R. and Futatsugi K. (1998) CafeOBJ report: The language, proof techniques, and methodologies for object-oriented algebraic specification, AMAST series in Computing 6, World Scientific.","DOI":"10.1142\/3831"},{"key":"S0960129507006305_ref13","doi-asserted-by":"publisher","DOI":"10.1023\/A:1024621922509"},{"key":"S0960129507006305_ref26","unstructured":"Reichel H. (1985) Behavioural validity of conditional equations in abstract data types. In: Contributions to general algebra 3, (Conference Proceedings, Vienna 1984), 301\u2013324."},{"key":"S0960129507006305_ref28","first-page":"252","volume-title":"Springer-Verlag Lecture Notes in Artificial Intelligence","author":"Ro\u015fu","year":"2000"},{"key":"S0960129507006305_ref29","unstructured":"Ro\u015fu G. and Goguen J. (2001) Circular coinduction. In: Proceedings, International Joint Conference on Automated Reasoning, IJCAR'01, Siena."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129507006305","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,29]],"date-time":"2019-03-29T15:39:50Z","timestamp":1553873990000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129507006305\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10]]},"references-count":30,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,10]]}},"alternative-id":["S0960129507006305"],"URL":"https:\/\/doi.org\/10.1017\/s0960129507006305","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10]]}}}