{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T04:02:22Z","timestamp":1746244942475,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548291"},{"type":"electronic","value":"9783642548307"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54830-7_18","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:30:31Z","timestamp":1395408631000},"page":"274-288","source":"Crossref","is-referenced-by-count":3,"title":["On Asymmetric Unification and the Combination Problem in Disjoint Theories"],"prefix":"10.1007","author":[{"given":"Serdar","family":"Erbatur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew M.","family":"Marshall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term rewriting and all that","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, New York (1998)"},{"issue":"2","key":"18_CR2","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F. Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. Journal of Symbolic Computation\u00a021(2), 211\u2013243 (1996)","journal-title":"Journal of Symbolic Computation"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification Theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445\u2013532. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: Proceedings of the 14th IEEE Workshop on Computer Security Foundations, CSFW 2001, pp. 82\u201396. IEEE Computer Society (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-40885-4_23","volume-title":"Frontiers of Combining Systems","author":"C. Bouchard","year":"2013","unstructured":"Bouchard, C., Gero, K.A., Lynch, C., Narendran, P.: On Forward Closure and the Finite Variant Property. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol.\u00a08152, pp. 327\u2013342. Springer, Heidelberg (2013)"},{"key":"18_CR6","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)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-33167-1_5","volume-title":"Computer Security \u2013 ESORICS 2012","author":"S. Erbatur","year":"2012","unstructured":"Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol.\u00a07459, pp. 73\u201390. Springer, Heidelberg (2012)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-38574-2_16","volume-title":"Automated Deduction \u2013 CADE-24","author":"S. Erbatur","year":"2013","unstructured":"Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C.A., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 231\u2013248. Springer, Heidelberg (2013)"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Erbatur, S., Kapur, D., Marshall, A.M., Meadows, C., Narendran, P., Ringeissen, C.: On Asymmetric Unification and the Combination Problem in Disjoint Theories. INRIA Research Report (2014), http:\/\/hal.inria.fr\/","DOI":"10.1007\/978-3-642-54830-7_18"},{"key":"18_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S. Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007\/2008\/2009. LNCS, vol.\u00a05705, pp. 1\u201350. Springer, Heidelberg (2009)"},{"issue":"3","key":"18_CR11","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.entcs.2009.05.015","volume":"238","author":"S. Escobar","year":"2009","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant Narrowing and Equational Unification. Electronic Notes Theor. Comput. Science\u00a0238(3), 103\u2013119 (2009)","journal-title":"Electronic Notes Theor. Comput. Science"},{"issue":"7-8","key":"18_CR12","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S. Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding Variant Narrowing and Optimal Variant Termination. J. Log. Algebr. Program.\u00a081(7-8), 898\u2013928 (2012)","journal-title":"J. Log. Algebr. Program."},{"issue":"1","key":"18_CR13","first-page":"61","volume":"2","author":"J.-P. Jouannaud","year":"2008","unstructured":"Jouannaud, J.-P., Toyama, Y.: Modular Church-Rosser Modulo: The Complete Picture. Int. J. Software and Informatics\u00a02(1), 61\u201375 (2008)","journal-title":"Int. J. Software and Informatics"},{"key":"18_CR14","unstructured":"Liu, Z.: Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis. PhD thesis, Clarkson University (2012)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S. Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 696\u2013701. Springer, Heidelberg (2013)"},{"key":"18_CR16","unstructured":"M\u00f6dersheim, S.: Models and methods for the automated analysis of security protocols. PhD thesis, ETH Zurich (2007)"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(87)90039-1","volume":"26","author":"M. Rusinowitch","year":"1987","unstructured":"Rusinowitch, M.: On Termination of the Direct sum of Term-Rewriting Systems. Information Processing Letters\u00a026, 65\u201370 (1987)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54830-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:46:50Z","timestamp":1746157610000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54830-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548291","9783642548307"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54830-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}