{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T11:14:12Z","timestamp":1648811652298},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,8,21]],"date-time":"2010-08-21T00:00:00Z","timestamp":1282348800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,3]]},"DOI":"10.1007\/s10817-010-9201-2","type":"journal-article","created":{"date-parts":[[2010,8,20]],"date-time":"2010-08-20T08:45:19Z","timestamp":1282293919000},"page":"363-390","source":"Crossref","is-referenced-by-count":2,"title":["E-unification with Constants vs. General E-unification"],"prefix":"10.1007","volume":"48","author":[{"given":"Jan","family":"Otop","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,8,21]]},"reference":[{"key":"9201_CR1","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1016\/0304-3975(88)90140-5","volume":"56","author":"F Baader","year":"1988","unstructured":"Baader, F., B\u00fcttner, W.: Unification in commutative idempotent monoids. Theor. Comput. Sci. 56, 345\u2013353 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"9201_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1999)","DOI":"10.1017\/CBO9781139172752"},{"key":"9201_CR3","series-title":"LNCS","volume-title":"11th CADE","author":"F Baader","year":"1992","unstructured":"Baader, F., Schulz, K.: Unification in the union of disjoint equational theories: combining decision procedures. In: 11th CADE. LNCS, vol. 607. Springer, Saratoga Springs, NY (1992)"},{"key":"9201_CR4","doi-asserted-by":"crossref","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. J. Symbol. Comput. 21, 211\u2013243 (1996)","journal-title":"J. Symbol. Comput."},{"key":"9201_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) A Chapter in Handbook of Automated Reasoning. Elsevier\/MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"9201_CR6","doi-asserted-by":"crossref","unstructured":"B\u00fcrckert H.-J., Herold A., Schmidt-Schauss, M.: On equational theories, unification and decidability. In: Proc. of the 2nd RTA. LNCS, vol. 256, pp. 204-215. Springer-Verlag (1987)","DOI":"10.1007\/3-540-17220-3_18"},{"key":"9201_CR7","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 2nd edn. Addison-Wesley (2001)","DOI":"10.1145\/568438.568455"},{"key":"9201_CR8","unstructured":"Kapur, D., Narendran, P.: Double-exponential complexity of computing a complete set of AC-unifiers. In: LICS, Santa Cruz, CA (1992)"},{"key":"9201_CR9","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1023\/A:1005764526878","volume":"19","author":"P Narendran","year":"1997","unstructured":"Narendran, P., Otto, F.: Single versus simultaneous equational unification and equational unification for variable-permuting theories. J. Autom. Reason. 19, 87\u2013115 (1997)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9201_CR10","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"9201_CR11","unstructured":"The RTA List of Open Problems: http:\/\/rtaloop.pps.jussieu.fr\/ . Accessed 15 September 2008"},{"issue":"1\/2","key":"9201_CR12","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M Schmidt-Schauss","year":"1989","unstructured":"Schmidt-Schauss, M.: Unification in a combination of arbitrary disjoint equational theories. J. Symbol. Comput. 8(1\/2), 51\u201399 (1989)","journal-title":"J. Symbol. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9201-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9201-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9201-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,10]],"date-time":"2020-06-10T18:48:07Z","timestamp":1591814887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9201-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,8,21]]},"references-count":12,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,3]]}},"alternative-id":["9201"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9201-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,8,21]]}}}