{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:32:29Z","timestamp":1761597149648,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642023477"},{"type":"electronic","value":"9783642023484"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02348-4_27","type":"book-chapter","created":{"date-parts":[[2009,6,18]],"date-time":"2009-06-18T07:27:21Z","timestamp":1245310041000},"page":"380-390","source":"Crossref","is-referenced-by-count":14,"title":["Unification and Narrowing in Maude 2.4"],"prefix":"10.1007","author":[{"given":"Manuel","family":"Clavel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francisco","family":"Dur\u00e1n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"Eker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Lincoln","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Narciso","family":"Mart\u00ed-Oliet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-70590-1_1","volume-title":"Rewriting Techniques and Applications","author":"M. Alpuente","year":"2008","unstructured":"Alpuente, M., Escobar, S., Iborra, J.: Modular termination of basic narrowing. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol.\u00a05117, pp. 1\u201316. Springer, Heidelberg (2008)"},{"unstructured":"Bae, K., Meseguer, J.: A rewriting-based model checker for the linear temporal logic of rewriting. In: Procs. of RULE 2008. ENTCS (to appear) (2008)","key":"27_CR2"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-540-78743-3_28","volume-title":"Fundamental Approaches to Software Engineering","author":"A. Boronat","year":"2008","unstructured":"Boronat, A., Meseguer, J.: An Algebraic semantics for MOF. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, pp. 377\u2013391. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Boudet, A., Contejean, E., Devie, H.: A new AC unification algorithm with an algorithm for solving systems of diophantine equations. In: Procs. of LICS 1990, pp. 289\u2013299 (1990)","key":"27_CR4","DOI":"10.1109\/LICS.1990.113755"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-48685-2_18","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"1999","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: The Maude system. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 240\u2013243. Springer, Heidelberg (1999)"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-44881-0_7","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"2003","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, J.: The Maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 14\u201329. Springer, Heidelberg (2003)"},{"key":"27_CR7","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)"},{"unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: Maude Manual (v. 2.4), SRI Intl. & U. of Illinois at Urbana-Champaign (October 2008), http:\/\/maude.cs.uiuc.edu","key":"27_CR8"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H. Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"issue":"1","key":"27_CR10","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/inco.1994.1067","volume":"113","author":"E. Contejean","year":"1994","unstructured":"Contejean, E., Devie, H.: An efficient incremental algorithm for solving systems of linear diophantine equations. Information and Computation\u00a0113(1), 143\u2013172 (1994)","journal-title":"Information and Computation"},{"unstructured":"Contejean, E., March\u00e9, C., Urbain, X.: CiME 3 (2004), http:\/\/cime.lri.fr\/","key":"27_CR11"},{"issue":"2","key":"27_CR12","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2006.07.002","volume":"66","author":"F. Dur\u00e1n","year":"2007","unstructured":"Dur\u00e1n, F., Meseguer, J.: Maude\u2019s module algebra. Sci. Comp. Progr.\u00a066(2), 125\u2013153 (2007)","journal-title":"Sci. Comp. Progr."},{"unstructured":"Eker, S.: Unification in Maude. Talk at the Protocol eXchange Seminar, Naval Postgraduate School (January 2007), http:\/\/maude.cs.uiuc.edu\/talks\/eker-unification.pdf","key":"27_CR13"},{"issue":"1-2","key":"27_CR14","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S. Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties. Theor. Comput. Sci.\u00a0367(1-2), 162\u2013202 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-73449-9_13","volume-title":"Term Rewriting and Applications","author":"S. Escobar","year":"2007","unstructured":"Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 153\u2013168. Springer, Heidelberg (2007)"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-540-70590-1_6","volume-title":"Rewriting Techniques and Applications","author":"S. Escobar","year":"2008","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Effectively checking the finite variant property. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol.\u00a05117, pp. 79\u201393. Springer, Heidelberg (2008)"},{"unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. In: Procs. of WRLA 2008, pp. 88\u2013102. ENTCS (2008)","key":"27_CR17"},{"key":"27_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0036921","volume-title":"Automata, Languages and Programming","author":"J.-P. Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: D\u00edaz, J. (ed.) ICALP 1983. LNCS, vol.\u00a0154, pp. 361\u2013373. Springer, Heidelberg (1983)"},{"key":"27_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol.\u00a087, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"doi-asserted-by":"crossref","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: Towards a strategy language for Maude. In: Procs. of WRLA 2004. ENTCS, vol.\u00a0117, pp. 417\u2013441 (2005)","key":"27_CR20","DOI":"10.1016\/j.entcs.2004.06.020"},{"issue":"3","key":"27_CR21","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.tcs.2006.12.018","volume":"373","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Ro\u015fu, G.: The rewriting logic semantics project. Theor. Comput. Sci.\u00a0373(3), 213\u2013237 (2007)","journal-title":"Theor. Comput. Sci."},{"issue":"1-2","key":"27_CR22","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. High.-Ord. Symb. Comp.\u00a020(1-2), 123\u2013160 (2007)","journal-title":"High.-Ord. Symb. Comp."},{"doi-asserted-by":"crossref","unstructured":"Rivera, J.E., Vallecillo, A.: Adding behavioral semantics to models. In: Procs. of EDOC 2007, pp. 169\u2013180 (2007)","key":"27_CR23","DOI":"10.1109\/EDOC.2007.40"},{"unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Information and Computation. (available online December 6, 2008) (in press)","key":"27_CR24"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-45446-2_27","volume-title":"Theoretical Computer Science","author":"E. Viola","year":"2001","unstructured":"Viola, E.: E-unifiability via narrowing. In: Restivo, A., Ronchi Della Rocca, S., Roversi, L. (eds.) ICTCS 2001. LNCS, vol.\u00a02202, pp. 426\u2013438. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02348-4_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T06:13:20Z","timestamp":1739168000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02348-4_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642023477","9783642023484"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02348-4_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}