{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:13:33Z","timestamp":1725567213707},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642340048"},{"type":"electronic","value":"9783642340055"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34005-5_9","type":"book-chapter","created":{"date-parts":[[2012,10,3]],"date-time":"2012-10-03T02:33:39Z","timestamp":1349231619000},"page":"162-181","source":"Crossref","is-referenced-by-count":4,"title":["Order-Sorted Equality Enrichments Modulo Axioms"],"prefix":"10.1007","author":[{"given":"Ra\u00fal","family":"Guti\u00e9rrez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Camilo","family":"Rocha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"9_CR2","series-title":"LNCS","first-page":"76","volume-title":"Proc. of the 7th International Colloquium on Automata, Languages and Programming, ICALP 1980","author":"J. Bergstra","year":"1980","unstructured":"Bergstra, J., Tucker, J.: Characterization of Computable Data Types by Means of a Finite Equational Specification Method. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a081, pp. 76\u201390. Springer, Heidelberg (1980)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"issue":"1-2","key":"9_CR4","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10990-008-9028-2","volume":"21","author":"F. Dur\u00e1n","year":"2008","unstructured":"Dur\u00e1n, F., Lucas, S., March\u00e9, C., Meseguer, J., Urbain, X.: Proving Operational Termination of Membership Equational Programs. Higher Order Symbolic Computation\u00a021(1-2), 59\u201388 (2008)","journal-title":"Higher Order Symbolic Computation"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-04222-5_15","volume-title":"Frontiers of Combining Systems","author":"F. Dur\u00e1n","year":"2009","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination Modulo Combinations of Equational Theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 246\u2013262. Springer, Heidelberg (2009)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and Coherence Properties of Conditional Order-Sorted Rewrite Theories. Journal of Logic and Algebraic Programming (2011) (to appear)","DOI":"10.1016\/j.jlap.2012.03.012"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J. Goguen","year":"1992","unstructured":"Goguen, J., Meseguer, J.: Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theoretical Computer Science\u00a0105, 217\u2013273 (1992)","journal-title":"Theoretical Computer Science"},{"key":"9_CR8","series-title":"LNCS","first-page":"356","volume-title":"Proc. of the 5th Conference on Automated Deduction, CADE 1980","author":"J.A. Goguen","year":"1980","unstructured":"Goguen, J.A.: How to Prove Algebraic Inductive Hypotheses Without Induction. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol.\u00a087, pp. 356\u2013373. Springer, Heidelberg (1980)"},{"key":"9_CR9","unstructured":"Guti\u00e9rrez, R., Meseguer, J., Rocha, C.: Order-Sorted Equality Enrichments Modulo Axioms (Extended Version). Tech. rep., University of Illinois at Urbana-Champaing (December 2011), \n                  \n                    http:\/\/hdl.handle.net\/2142\/28597"},{"key":"9_CR10","unstructured":"Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL, USA (2008)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-540-32033-3_13","volume-title":"Term Rewriting and Applications","author":"J. Hendrix","year":"2005","unstructured":"Hendrix, J., Clavel, M., Meseguer, J.: A Sufficient Completeness Reasoning Tool for Partial Specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 165\u2013174. Springer, Heidelberg (2005)"},{"issue":"4","key":"9_CR12","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1016\/j.ipl.2005.05.002","volume":"95","author":"S. Lucas","year":"2005","unstructured":"Lucas, S., March\u00e9, C., Meseguer, J.: Operational Termination of Conditional Term Rewriting Systems. Information Processing Letters\u00a095(4), 446\u2013453 (2005)","journal-title":"Information Processing Letters"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership Algebra as a Logical Framework for Equational Specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"9_CR14","unstructured":"Meseguer, J., Goguen, J.A.: Initially, Induction and Computability. Algebraic Methods in Semantics (1986)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Musser, D.R.: On Proving Inductive Properties of Abstract Data Types. In: Proc. of the 7th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1980, pp. 154\u2013162. ACM Press (1980)","DOI":"10.1145\/567446.567461"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-540-75292-9_26","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2007","author":"N. Masaki","year":"2007","unstructured":"Masaki, N., Kokichi, F.: On Equality Predicates in Algebraic Specification Languages. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol.\u00a04711, pp. 381\u2013395. Springer, Heidelberg (2007)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78913-0_25","volume-title":"Relations and Kleene Algebra in Computer Science","author":"C. Rocha","year":"2008","unstructured":"Rocha, C., Meseguer, J.: Theorem Proving Modulo Based on Boolean Equational Procedures. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS\/AKA 2008. LNCS, vol.\u00a04988, pp. 337\u2013351. Springer, Heidelberg (2008)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-642-22944-2_22","volume-title":"Algebra and Coalgebra in Computer Science","author":"C. Rocha","year":"2011","unstructured":"Rocha, C., Meseguer, J.: Proving Safety Properties of Rewrite Theories. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol.\u00a06859, pp. 314\u2013328. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34005-5_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:40:42Z","timestamp":1620132042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34005-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340048","9783642340055"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34005-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}