{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T05:37:40Z","timestamp":1726033060877},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030221010"},{"type":"electronic","value":"9783030221027"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-22102-7_26","type":"book-chapter","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T08:21:26Z","timestamp":1561450886000},"page":"562-572","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Note on Unification, Subsumption and Unification Type"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,1]]},"reference":[{"issue":"3","key":"26_CR1","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BF02328451","volume":"2","author":"F Baader","year":"1986","unstructured":"Baader, F.: The theory of idempotent semigroups is of unification type zero. J. Autom. Reasoning 2(3), 283\u2013286 (1986)","journal-title":"J. Autom. Reasoning"},{"issue":"5","key":"26_CR2","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1016\/S0747-7171(89)80055-0","volume":"8","author":"F Baader","year":"1989","unstructured":"Baader, F.: Unification in commutative theories. J. Symb. Comput. 8(5), 479\u2013497 (1989)","journal-title":"J. Symb. Comput."},{"key":"26_CR3","unstructured":"Baader, F.: Remarks on ACUI, personal communication (2016)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Franz, B., Borgwardt, S., Morawska, B.: Extending unification in EL to disunification: the case of dismatching and local disunification. Log. Methods Comput. Sci. 12(4) (2016)","DOI":"10.2168\/LMCS-12(4:1)2016"},{"key":"26_CR5","unstructured":"Baader, F., Ludmann, P.: The exact unification type of commutative theories. In: Ghilardi, S., Schmidt-Schau\u00df, M. (eds.) Informal Proceedings of the 30th International Workshop on Unification (UNIF 2016) (2016)"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-642-02348-4_25","volume-title":"Rewriting Techniques and Applications","author":"F Baader","year":"2009","unstructured":"Baader, F., Morawska, B.: Unification in the description logic \n                    \n                      \n                    \n                    $$\\cal{EL}$$\n                  . In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 350\u2013364. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-02348-4_25"},{"key":"26_CR7","doi-asserted-by":"publisher","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, Cambridge (1998)"},{"key":"26_CR8","unstructured":"Baader, F., Siekmann, J.H.: Unification theory. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A., Siekmann, J.H. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, Deduction Methodologies, vol. 2, pp. 41\u2013126. Oxford University Press (1994)"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 445\u2013532. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"26_CR10","unstructured":"Cabrer, L.M., Metcalfe, G.: From admissibility to a new hierarchy of unification types. In: Kutsia, T., Ringeissen, C. (eds.) Proceedings of the 28\n                    \n                      \n                    \n                    $$^{th}$$\n                   International Workshop on Unification (UNIF 2014) (2014)"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Cabrer, L.M., Metcalfe, G.: Exact unification and admissibility. Log. Methods Comput. Sci. 11(3) (2015)","DOI":"10.2168\/LMCS-11(3:23)2015"},{"issue":"2\u20133","key":"26_CR12","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/j.tcs.2008.05.012","volume":"403","author":"C Calv\u00e8s","year":"2008","unstructured":"Calv\u00e8s, C., Fern\u00e1ndez, M.: A polynomial nominal unification algorithm. Theor. Comput. Sci. 403(2\u20133), 285\u2013306 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR13","series-title":"Informatik-Fachberichte","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-69391-5_18","volume-title":"GWAI-83","author":"E Eder","year":"1983","unstructured":"Eder, E.: Properties of Substitutions and unifications. In: Neumann, B. (ed.) GWAI-83. Informatik-Fachberichte, vol. 76, pp. 197\u2013206. Springer, Heidelberg (1983). \n                    https:\/\/doi.org\/10.1007\/978-3-642-69391-5_18"},{"key":"26_CR14","unstructured":"Levy, J., Villaret, M.: An efficient nominal unification algorithm. In: Lynch, C. (ed.) Proceedings of the 21st RTA, volume 6 of LIPIcs, pp. 209\u2013226. Schloss Dagstuhl (2010)"},{"issue":"3","key":"26_CR15","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/BF02328450","volume":"2","author":"M Schmidt-Schau\u00df","year":"1986","unstructured":"Schmidt-Schau\u00df, M.: Unification under associativity and idempotence is of type nullary. J. Autom. Reasoning 2(3), 277\u2013281 (1986)","journal-title":"J. Autom. Reasoning"},{"key":"26_CR16","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.jsc.2018.04.003","volume":"90","author":"M Schmidt-Schau\u00df","year":"2019","unstructured":"Schmidt-Schau\u00df, M., Sabel, D., Kutz, Y.D.K.: Nominal unification with atom-variables. J. Symb. Comput. 90, 42\u201364 (2019)","journal-title":"J. Symb. Comput."},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-540-45220-1_41","volume-title":"Computer Science Logic","author":"C Urban","year":"2003","unstructured":"Urban, C., Pitts, A., Gabbay, M.: Nominal unification. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 513\u2013527. Springer, Heidelberg (2003). \n                    https:\/\/doi.org\/10.1007\/978-3-540-45220-1_41"}],"container-title":["Lecture Notes in Computer Science","Description Logic, Theory Combination, and All That"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-22102-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T08:26:25Z","timestamp":1561451185000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-22102-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030221010","9783030221027"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-22102-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"1 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}