{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:21Z","timestamp":1761611301154},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584315"},{"type":"electronic","value":"9783540487913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58431-5_6","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:06:38Z","timestamp":1330272398000},"page":"41-58","source":"Crossref","is-referenced-by-count":9,"title":["Proving behavioural theorems with standard first-order logic"],"prefix":"10.1007","author":[{"given":"Michel","family":"Bidoit","sequence":"first","affiliation":[]},{"given":"Rolf","family":"Hennicker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"B. Bauer and R. Hennicker. Proving the correctness of algebraic implementations by the ISAR system. In Proc. of DISCO'93, pages 2\u201316. Springer-Verlag L.N.C.S. 722, 1993.","DOI":"10.1007\/BFb0013164"},{"key":"6_CR2","unstructured":"G. Bernot and M. Bidoit. Proving the correctness of algebraically specified software: modularity and observability issues. In Proc. of AMAST'91, pages 216\u2013242. Springer-Verlag Workshops in Computing Series, 1992."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"G. Bernot, M. Bidoit, and T. Knapik. Towards an adequate notion of observation. In Proc. of ESOP'92, pages 39\u201355. Springer-Verlag L.N.C.S. 582, 1992.","DOI":"10.1007\/3-540-55253-7_3"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"M. Bidoit and R. Hennicker. How to prove observational theorems with LP. In Proc. of the First International Workshop on Larch. Springer-Verlag Workshops in Computing Series, 1993.","DOI":"10.1007\/978-1-4471-3558-6_2"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"M. Bidoit, R. Hennicker, and M. Wirsing. Characterizing behavioural semantics and abstractor semantics. In Proc. of ESOP'94, pages 105\u2013119. Springer-Verlag L.N.C.S. 788, 1994.","DOI":"10.1007\/3-540-57880-3_7"},{"key":"6_CR6","unstructured":"H. Ehrig and B. Mahr. Fundamentals of algebraic specification 1. Equations and initial semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985."},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"S. Garland and J. Guttag. An overview of LP, the Larch Prover. In Proc. of the Third International Conference on Rewriting Techniques and Applications, pages 137\u2013151. Springer-Verlag L.N.C.S. 355, 1989.","DOI":"10.1007\/3-540-51081-8_105"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"J. Goguen and J. Meseguer. Universal realization, persistent interconnection and implementation of abstract modules. In Proc. of 9th ICALP, pages 265\u2013281. Springer-Verlag L.N.C.S. 140, 1982.","DOI":"10.1007\/BFb0012775"},{"key":"6_CR9","unstructured":"J.A. Goguen, J.W. Thatcher, and E.G. Wagner. An initial approach to the specification, correctness, and implementation of abstract data types, volume 4 of Current Trends in Programming Methodology. Prentice Hall, 1978."},{"issue":"4","key":"6_CR10","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/BF01642507","volume":"3","author":"R. Hennicker","year":"1991","unstructured":"R. Hennicker. Context induction: a proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing, 3(4):326\u2013345, 1991.","journal-title":"Formal Aspects of Computing"},{"key":"6_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","volume":"4","author":"R. Milner","year":"1977","unstructured":"R. Milner. Fully abstract models of typed \u03bb-calculi. Theoretical Computer Science, 4:1\u201322, 1977.","journal-title":"Theoretical Computer Science"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"P. Nivela and F. Orejas. Initial behaviour semantics for algebraic specification. In Recent Trends in Data Type Specification, pages 184\u2013207. Springer-Verlag L.N.C.S. 332, 1988.","DOI":"10.1007\/3-540-50325-0_10"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"F. Orejas, M. Navarro, and A. S\u00e0nches. Implementation and behavioural equivalence: A survey. In Recent Trends in Data Type Specification, pages 93\u2013125. Springer-Verlag L.N.C.S. 655, 1993.","DOI":"10.1007\/3-540-56379-2_36"},{"key":"6_CR14","unstructured":"H. Reichel. Initial restrictions of behaviour. In Proc. of IFIP Working Conference, The Role of Abstract Models in Information Processing, 1985."},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"D. Sannella and A. Tarlecki. On observational equivalence and algebraic specification. In Proc. of TAPSOFT'85, pages 308\u2013322. Springer-Verlag L.N.C.S. 185, 1985.","DOI":"10.1007\/3-540-15198-2_20"},{"key":"6_CR16","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/0167-6423(90)90057-K","volume":"14","author":"O. Schoett","year":"1990","unstructured":"O. Schoett. Behavioural correctness of data representation. Science of Computer Programming, 14:43\u201357, 1990.","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Algebraic and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58431-5_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:21:05Z","timestamp":1605648065000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58431-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584315","9783540487913"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-58431-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}