{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:19:34Z","timestamp":1725567574029},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_8","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T12:51:59Z","timestamp":1286196719000},"page":"97-111","source":"Crossref","is-referenced-by-count":8,"title":["SAT Encoding of Unification in $\\mathcal{EL}$"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"Morawska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F.: Terminological cycles in a description logic with existential restrictions. In: Proc. IJCAI\u00a02003. Morgan Kaufmann, Los Altos (2003)","DOI":"10.25368\/2022.120"},{"key":"8_CR2","unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the $\\mathcal{EL}$ envelope. In: Proc. IJCAI\u00a02005. Morgan Kaufmann, Los Altos (2005)"},{"volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","year":"2003","key":"8_CR3","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"8_CR4","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 $\\mathcal{EL}$ . In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 350\u2013364. Springer, Heidelberg (2009)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., Morawska, B.: Unification in the description logic $\\mathcal{EL}$ . In: Logical Methods in Computer Science (to appear, 2010)","DOI":"10.2168\/LMCS-6(3:17)2010"},{"issue":"3","key":"8_CR6","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1006\/jsco.2000.0426","volume":"31","author":"F. Baader","year":"2001","unstructured":"Baader, F., Narendran, P.: Unification of concepts terms in description logics. J. of Symbolic Computation\u00a031(3), 277\u2013305 (2001)","journal-title":"J. of Symbolic Computation"},{"issue":"2","key":"8_CR7","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.: Unification in the union of disjoint equational theories: Combining decision procedures. J. of Symbolic Computation\u00a021(2), 211\u2013243 (1996)","journal-title":"J. of Symbolic Computation"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning, vol.\u00a0I. Elsevier Science Publishers, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BF00245463","volume":"9","author":"D. Kapur","year":"1992","unstructured":"Kapur, D., Narendran, P.: Complexity of unification problems with associative-commutative operators. J. Automated Reasoning\u00a09, 261\u2013288 (1992)","journal-title":"J. Automated Reasoning"},{"key":"8_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/3-540-44613-3_3","volume-title":"Non-Standard Inferences in Description Logics","year":"2001","unstructured":"K\u00fcsters, R. (ed.): Non-Standard Inferences in Description Logics. LNCS (LNAI), vol.\u00a02100, p. 33. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T15:53:25Z","timestamp":1685807605000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}