{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T11:23:50Z","timestamp":1725708230944},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642351006"},{"type":"electronic","value":"9783642351013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35101-3_42","type":"book-chapter","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T11:40:16Z","timestamp":1354189216000},"page":"493-504","source":"Crossref","is-referenced-by-count":5,"title":["A Goal-Oriented Algorithm for Unification in $\\mathcal{ELH}_{R+}$ w.r.t. Cycle-Restricted Ontologies"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Borgwardt","sequence":"additional","affiliation":[]},{"given":"Barbara","family":"Morawska","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"42_CR1","unstructured":"Baader, F., Borgwardt, S., Mendez, J., Morawska, B.: UEL: Unification solver for \n \n \n \n $\\mathcal{EL}$\n . In: Proc. DL 2012. CEUR Workshop Proceedings, vol.\u00a0846 (2012)"},{"key":"42_CR2","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: Extending unification in \n \n \n \n $\\mathcal{EL}$\n towards general TBoxes. In: Proc. KR 2012, pp. 568\u2013572. AAAI Press (2012) (short paper)"},{"key":"42_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: A goal-oriented algorithm for unification in \n \n \n \n $\\mathcal{ELH}_{R+}$\n w.r.t. cycle-restricted ontologies. LTCS-Report 12-05, TU Dresden, Germany (2012), \n \n http:\/\/lat.inf.tu-dresden.de\/research\/reports.html","DOI":"10.1007\/978-3-642-31365-3_5"},{"key":"42_CR4","doi-asserted-by":"crossref","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: A goal-oriented algorithm for unification in \n \n \n \n $\\mathcal{EL}$\n w.r.t. cycle-restricted TBoxes. In: Proc. DL 2012. CEUR Workshop Proceedings, vol.\u00a0846 (2012)","DOI":"10.1007\/978-3-642-35101-3_42"},{"key":"42_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-31365-3_5","volume-title":"Automated Reasoning","author":"F. Baader","year":"2012","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. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 30\u201344. Springer, Heidelberg (2012)"},{"key":"42_CR6","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, TU Dresden, Germany (2012), \n \n http:\/\/lat.inf.tu-dresden.de\/research\/reports.html","DOI":"10.1007\/978-3-642-31365-3_5"},{"key":"42_CR7","unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the \n \n \n \n $\\mathcal{EL}$\n envelope. In: Proc. IJCAI 2005, pp. 364\u2013369. Morgan Kaufmann (2005)"},{"key":"42_CR8","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":"42_CR9","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)"},{"key":"42_CR10","doi-asserted-by":"crossref","unstructured":"Baader, F., Morawska, B.: Unification in the description logic \n \n \n \n $\\mathcal{EL}$\n . Log. Meth. Comput. Sci.\u00a06(3) (2010)","DOI":"10.2168\/LMCS-6(3:17)2010"},{"issue":"3","key":"42_CR11","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. Symb. Comput.\u00a031(3), 277\u2013305 (2001)","journal-title":"J. Symb. Comput."},{"key":"42_CR12","unstructured":"Brandt, S.: Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and\u2014what else? In: Proc. ECAI 2004, pp. 298\u2013302 (2004)"},{"key":"42_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/11551263_5","volume-title":"KI 2005: Advances in Artificial Intelligence","author":"S. Brandt","year":"2005","unstructured":"Brandt, S., Model, J.: Subsumption in \n \n \n \n $\\cal EL$\n w.r.t. hybrid TBoxes. In: Furbach, U. (ed.) KI 2005. LNCS (LNAI), vol.\u00a03698, pp. 34\u201348. Springer, Heidelberg (2005)"},{"key":"42_CR14","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Handbook of Knowledge Representation, pp. 89\u2013134. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03002-7"},{"key":"42_CR15","unstructured":"Hofmann, M.: Proof-theoretic approach to description-logic. In: Proc. LICS 2005. pp. 229\u2013237. IEEE Press (2005)"},{"issue":"1","key":"42_CR16","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10817-007-9068-z","volume":"39","author":"B. Morawska","year":"2007","unstructured":"Morawska, B.: General E-unification with eager variable elimination and a nice cycle rule. J. Autom. Reasoning\u00a039(1), 77\u2013106 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"42_CR17","unstructured":"Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Proc. IJCAI 1991, pp. 466\u2013471 (1991)"},{"key":"42_CR18","doi-asserted-by":"crossref","unstructured":"Wolter, F., Zakharyaschev, M.: Undecidability of the unification and admissibility problems for modal and description logics. ACM Trans. Comput. Log. 9(4) (2008)","DOI":"10.1145\/1380572.1380574"}],"container-title":["Lecture Notes in Computer Science","AI 2012: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35101-3_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,9]],"date-time":"2019-05-09T05:54:25Z","timestamp":1557381265000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35101-3_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642351006","9783642351013"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35101-3_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}