{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:02:46Z","timestamp":1725663766686},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540552536"},{"type":"electronic","value":"9783540468035"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55253-7_11","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T09:56:34Z","timestamp":1330250194000},"page":"182-199","source":"Crossref","is-referenced-by-count":4,"title":["ELIOS-OBJ theorem proving in a specification language"],"prefix":"10.1007","author":[{"given":"I.","family":"Gnaedig","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"11_CR1","first-page":"192","volume-title":"Lecture Notes in Computer Science","author":"L. Bachmair","year":"1987","unstructured":"L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. In Proceedings 2nd Conference on Rewriting Techniques and Applications, Bordeaux (France), volume 256 of Lecture Notes in Computer Science, pages 192\u2013203, Bordeaux (France), May 1987. Springer-Verlag."},{"issue":"1","key":"11_CR2","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1 & 2):69\u2013116, 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"11_CR3","unstructured":"R. Forgaard and J. Guttag. Reve: A term rewriting system generator with failure-resistant Knuth-Bendix. Technical report, MIT-LCS, 1984."},{"key":"11_CR4","unstructured":"H. Ganzinger and R. Giegerich. A note on termination in combinations of heterogeneous term rewriting systems. Bulletin of European Association for Theoretical Computer Science, 31, February 1987."},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"I. Gnaedig, C. Kirchner, and H. Kirchner. Equational completion in order-sorted algebras. In M. Dauchet and M. Nivat, editors, Proceedings of the 13th Colloquium on Trees in Algebra and Programming, volume 299 of Lecture Notes in Computer Science, pages 165\u2013184. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0026103"},{"key":"11_CR6","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/0304-3975(90)90034-F","volume":"72","author":"I. Gnaedig","year":"1990","unstructured":"I. Gnaedig, C. Kirchner, and H. Kirchner. Equational completion in order-sorted algebras. Theoretical Computer Science, 72:169\u2013202, 1990.","journal-title":"Theoretical Computer Science"},{"key":"11_CR7","unstructured":"J.A. Goguen and J. Meseguer. Order-sorted algebra I: Partial and overloaded operations, errors and inheritance. Technical report, SRI International, Computer Science Lab, 1988. Given as lecture at a Seminar on Types, Carnegie-Mellon University, June 1983."},{"key":"11_CR8","volume-title":"Technical Report SRI-CSL-88-9","author":"J. A. Goguen","year":"1988","unstructured":"J.A. Goguen and T. Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, 333, Ravenswood Ave., Menlo Park, CA 94025, August 1988."},{"key":"11_CR9","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/B978-0-12-115350-2.50017-8","volume-title":"Formal Language Theory: Perspectives and Open Problems","author":"G. Huet","year":"1980","unstructured":"G. Huet and D. Oppen. Equations and rewrite rules: A survey. In R.V. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349\u2013405. Academic Press, New York, 1980."},{"key":"11_CR10","unstructured":"S. Kamin and J.-J. L\u00e9vy. Attempts for generalizing the recursive path ordering. Inria, Rocquencourt, 1982."},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ-3. In Proceedings of 15th International Colloquium on Automata, Languages and Programming, volume 317 of Lecture Notes in Computer Science, pages 287\u2013301. Springer-Verlag, 1988.","DOI":"10.1007\/3-540-19488-6_123"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"P. Lescanne. Computer experiments with the REVE term rewriting systems generator. In Proceedings of 10th ACM Symposium on Principles of Programming Languages, pages 99\u2013108. Association for Computing Machinery, 1983.","DOI":"10.1145\/567067.567078"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"P. Lescanne. Implementation of completion by transition rules + control: ORME. In H. Kirchner and W. Wechler, editors, Proceedings 2nd International Workshop on Algebraic and Logic Programming, Nancy (France), volume 463 of Lecture Notes in Computer Science, pages 262\u2013269. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-53162-9_44"},{"issue":"2","key":"11_CR14","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(87)90039-1","volume":"26","author":"M. Rusinowitch","year":"1987","unstructured":"M. Rusinowitch. On termination of the direct sum of term rewriting systems. Information Processing Letters, 26(2):65\u20137G, 1987.","journal-title":"Information Processing Letters"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Y. Toyama, J.W. Klop, and H.P. Barendregt. Termination for the direct sum of left-linear term rewriting systems. In N. Dershowitz, editor, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (North Carolina, USA), volume 355 of Lecture Notes in Computer Science, pages 477\u2013491. Springer-Verlag, April 1989.","DOI":"10.1007\/3-540-51081-8_127"}],"container-title":["Lecture Notes in Computer Science","ESOP '92"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55253-7_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:58:23Z","timestamp":1605646703000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55253-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540552536","9783540468035"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-55253-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}