{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:29:44Z","timestamp":1725892184259},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313646"},{"type":"electronic","value":"9783642313653"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31365-3_5","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T20:35:34Z","timestamp":1340310934000},"page":"30-44","source":"Crossref","is-referenced-by-count":5,"title":["SAT Encoding of Unification in $\\mathcal{ELH}_{{R}^+}$ w.r.t. Cycle-Restricted Ontologies"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Borgwardt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"Morawska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: Unification in the description logic \n                    \n                      \n                    \n                    $\\mathcal{EL}$\n                   w.r.t. cycle-restricted TBoxes. LTCS-Report 11-05, Theoretical Computer Science, TU Dresden (2011), \n                    \n                      http:\/\/lat.inf.tu-dresden.de\/research\/reports.html","key":"5_CR1","DOI":"10.1007\/978-3-642-22438-6_8"},{"unstructured":"Baader, F., Borgwardt, S., Morawska, B.: Extending unification in \n                    \n                      \n                    \n                    $\\mathcal{EL}$\n                   towards general TBoxes. In: Proc. of the 13th Int. Conf. on Principles of Knowledge Representation and Reasoning. AAAI Press (2012) (short paper)","key":"5_CR2"},{"doi-asserted-by":"crossref","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: SAT encoding of unification in \n                    \n                      \n                    \n                    $\\mathcal{ELH}_{{R}^{+}}$\n                   w.r.t. cycle-restricted ontologies. LTCS-Report 12-02, Theoretical Computer Science, TU Dresden (2012), \n                    \n                      http:\/\/lat.inf.tu-dresden.de\/research\/reports.html","key":"5_CR3","DOI":"10.1007\/978-3-642-31365-3_5"},{"key":"5_CR4","first-page":"364","volume-title":"Proc. of the 19th Int. Joint Conf. on Artificial Intelligence","author":"F. Baader","year":"2005","unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the \n                    \n                      \n                    \n                    $\\mathcal{EL}$\n                   envelope. In: Kaelbling, L.P., Saffiotti, A. (eds.) Proc. of the 19th Int. Joint Conf. on Artificial Intelligence, pp. 364\u2013369. Morgan Kaufmann, Los Altos (2005)"},{"key":"5_CR5","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                    $\\mathcal{EL}$\n                  . In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 350\u2013364. Springer, Heidelberg (2009)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-16242-8_8","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F. Baader","year":"2010","unstructured":"Baader, F., Morawska, B.: SAT Encoding of Unification in \n                    \n                      \n                    \n                    $\\mathcal{EL}$\n                  . In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 97\u2013111. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Baader, F., Morawska, B.: Unification in the description logic \n                    \n                      \n                    \n                    $\\mathcal{EL}$\n                  . Logical Methods in Computer Science 6(3) (2010)","key":"5_CR7","DOI":"10.2168\/LMCS-6(3:17)2010"},{"issue":"3","key":"5_CR8","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 concept terms in description logics. J. of Symbolic Computation\u00a031(3), 277\u2013305 (2001)","journal-title":"J. of Symbolic Computation"},{"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. The MIT Press (2001)","key":"5_CR9","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press (2009)","key":"5_CR10"},{"unstructured":"Brandt, S.: Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and\u2014what else? In: de\u00a0M\u00e1ntaras, R.L., Saitta, L. (eds.) Proc. of the 16th Eur. Conf. on Artificial Intelligence. pp. 298\u2013302 (2004)","key":"5_CR11"},{"unstructured":"Campbell, J.R., Lopez Osornio, A., de Quiros, F., Luna, D., Reynoso, G.: Semantic interoperability and SNOMED\u00a0CT: A case study in clinical problem lists. In: Kuhn, K., Warren, J., Leong, T.Y. (eds.) Proc. of the 12th World Congress on Health (Medical) Informatics, pp. 2401\u20132402. IOS Press (2007)","key":"5_CR12"},{"issue":"1&2","key":"5_CR13","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","volume":"166","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A., Voronkov, A.: The undecidability of simultaneous rigid E-unification. Theor. Comput. Sci.\u00a0166(1&2), 291\u2013300 (1996)","journal-title":"Theor. Comput. Sci."},{"issue":"1\/2","key":"5_CR14","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0890-5401(90)90061-L","volume":"87","author":"J.H. Gallier","year":"1990","unstructured":"Gallier, J.H., Narendran, P., Plaisted, D.A., Snyder, W.: Rigid E-unification: NP-completeness and applications to equational matings. Inf. Comput.\u00a087(1\/2), 129\u2013195 (1990)","journal-title":"Inf. Comput."},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/11901181_20","volume-title":"Conceptual Modeling - ER 2006","author":"J. Seidenberg","year":"2006","unstructured":"Seidenberg, J., Rector, A.L.: Representing Transitive Propagation in OWL. In: Embley, D.W., Oliv\u00e9, A., Ram, S. (eds.) ER 2006. LNCS, vol.\u00a04215, pp. 255\u2013266. Springer, Heidelberg (2006)"},{"unstructured":"Sofronie-Stokkermans, V.: Locality and subsumption testing in \n                    \n                      \n                    \n                    $\\mathcal{EL}$\n                   and some of its extensions. In: Proc. Advances in Modal Logic (2008)","key":"5_CR16"},{"key":"5_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-73599-1_38","volume-title":"Artificial Intelligence in Medicine","author":"B. Suntisrivaraporn","year":"2007","unstructured":"Suntisrivaraporn, B., Baader, F., Schulz, S., Spackman, K.: Replacing SEP-Triplets in SNOMED CT Using Tractable Description Logic Operators. In: Bellazzi, R., Abu-Hanna, A., Hunter, J. (eds.) AIME 2007. LNCS (LNAI), vol.\u00a04594, pp. 287\u2013291. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31365-3_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:58:33Z","timestamp":1620129513000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31365-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313646","9783642313653"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31365-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}