{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,9]],"date-time":"2026-10-09T16:50:16Z","timestamp":1791564616445,"version":"4.3.4"},"reference-count":28,"publisher":"Duke University Press","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Notre Dame J. Formal Logic"],"published-print":{"date-parts":[[2016,1,1]]},"abstract":"<jats:p>Unification in description logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The inexpressive description logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has been shown to be NP-complete and, thus, of considerably lower complexity than unification in other description logics of similarly restricted expressive power. However, EL allows the use of the top concept (\u22a4), which represents the whole interpretation domain, whereas the large medical ontology SNOMED\u2009CT makes no use of this feature. Surprisingly, removing the top concept from EL makes the unification problem considerably harder. More precisely, we will show that unification in EL without the top concept is PSPACE-complete. In addition to the decision problem, we also consider the problem of actually computing EL\u2212\u22a4-unifiers.<\/jats:p>","DOI":"10.1215\/00294527-3555507","type":"journal-article","created":{"date-parts":[[2016,7,19]],"date-time":"2016-07-19T14:17:05Z","timestamp":1468937825000},"page":"443-476","source":"Crossref","is-referenced-by-count":2,"title":["Deciding Unifiability and Computing Local Unifiers in the Description Logic EL without Top Constructor"],"prefix":"10.1215","volume":"57","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nguyen Thanh","family":"Binh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Borgwardt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Barbara","family":"Morawska","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"73","reference":[{"key":"1","unstructured":"[1] Baader, F., \u201cTerminological cycles in a description logic with existential restrictions,\u201d pp. 325\u201330 in <i>Proceedings of the 18th International Joint Conference on Artificial Intelligence<\/i> (<i>IJCAI\u201903<\/i>), edited by G. Gottlob and T. Walsh, Morgan Kaufmann, San Francisco, Calif., 2003."},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] Baader, F., N. T. Binh, S. Borgwardt, and B. Morawska, \u201cComputing local unifiers in the description logic $\\mathcal{EL}$ without the top concept,\u201d pp. 2\u20138 in <i>Proceedings of the 25th International Workshop on Unification<\/i> (<i>UNIF\u201911<\/i>), edited by F. Baader, B. Morawska, and J. Otop, 2011.","DOI":"10.1007\/978-3-642-22438-6_8"},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] Baader, F., N. T. Binh, S. Borgwardt, and B. Morawska, \u201cUnification in the description logic $\\mathcal{EL}$ without the top concept,\u201d pp. 70\u201384 in <i>Automated Deduction\u2014CADE-23<\/i>, edited by N. Bj\u00f8rner and V. Sofronie-Stokkermans, vol. 6803 of <i>Lecture Notes in Computer Science<\/i>, Springer, Heidelberg, 2011.","DOI":"10.1007\/978-3-642-22438-6_8"},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] Baader, F., S. Borgwardt, and B. Morawska, \u201cA goal-oriented algorithm for unification in $\\mathcal{ELH}_{R^{+}}$ w.r.t. cycle-restricted ontologies,\u201d pp. 493\u2013504 in <i>AI 2012: Advances in Artificial Intelligence<\/i>, edited by M. Thielscher and D. Zhang, vol. 7691 of <i>Lecture Notes in Computer Science<\/i>, Springer, Heidelberg, 2012.","DOI":"10.1007\/978-3-642-35101-3_42"},{"key":"5","doi-asserted-by":"publisher","unstructured":"[5] Baader, F., S. Borgwardt, and B. Morawska, \u201cSAT- encoding of unification in $\\mathcal{ELH}_{R^{+}}$ w.r.t. cycle-restricted ontologies,\u201d pp. 30\u201344 in <i>Automated Reasoning<\/i>, edited by B. Gramlich, D. Miller, and U. Sattler, vol. 7364 of <i>Lecture Notes in Computer Science<\/i>, Springer, Heidelberg, 2012.","DOI":"10.1007\/978-3-642-31365-3_5"},{"key":"6","unstructured":"[6] Baader, F., S. Borgwardt, and B. Morawska, \u201cExtending unification in $\\mathcal{EL}$ towards general TBoxes,\u201d pp. 568\u201372 in <i>Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201912)<\/i>, edited by G. Brewka, T. Eiter, and S. A. McIlraith, AAAI Press, Palo Alto, Calif., 2012."},{"key":"7","unstructured":"[7] Baader, F., S. Brandt, and C. Lutz, \u201cPushing the $\\mathcal{EL}$ envelope,\u201d pp. 364\u201369 in <i>Proceedings of the 19th International Joint Conference on Artificial Intelligence<\/i> (<i>IJCAI\u201905<\/i>), edited by L. P. Kaelbling and A. Saffiotti, Morgan Kaufmann, San Francisco, Calif., 2005."},{"key":"8","unstructured":"[8] Baader, F., D. Calvanese, D. McGuinness, D. Nardi, and P. F. Patel-Schneider, eds., <i>The Description Logic Handbook: Theory, Implementation, and Applications<\/i>, Cambridge University Press, Cambridge, 2003."},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] Baader, F., and S. Ghilardi, \u201cUnification in modal and description logics,\u201d <i>Logic Journal of the IGPL<\/i>, vol. 19 (2011), pp. 705\u201330.","DOI":"10.1093\/jigpal\/jzq008"},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] Baader, F., and B. Morawska, \u201cUnification in the description logic $\\mathcal{EL}$,\u201d pp. 350\u201364 in <i>Rewriting Techniques and Applications<\/i>, edited by R. Treinen, vol. 5595 of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 2009.","DOI":"10.1007\/978-3-642-02348-4_25"},{"key":"11","doi-asserted-by":"publisher","unstructured":"[11] Baader, F., and B. Morawska, \u201cSAT encoding of unification in $\\mathcal{EL}$,\u201d pp. 97\u2013111 in <i>Logic for Programming, Artificial Intelligence, and Reasoning<\/i>, edited by C. G. Ferm\u00fcller and A. Voronkov, vol. 6397of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 2010.","DOI":"10.1007\/978-3-642-16242-8_8"},{"key":"12","doi-asserted-by":"publisher","unstructured":"[12] Baader, F., and B. Morawska, \u201cUnification in the description logic $\\mathcal{EL}$,\u201d <i>Logical Methods in Computer Science<\/i>, vol. 6 (2010), no. 17.","DOI":"10.2168\/LMCS-6(3:17)2010"},{"key":"13","doi-asserted-by":"publisher","unstructured":"[13] Baader, F., and P. Narendran, \u201cUnification of concept terms in description logics,\u201d <i>Journal of Symbolic Computation<\/i>, vol. 31 (2001), pp. 277\u2013305.","DOI":"10.1006\/jsco.2000.0426"},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] Baader, F., and W. Snyder, \u201cUnification theory,\u201d pp. 445\u2013532 in <i>Handbook of Automated Reasoning<\/i>, edited by J. A. Robinson and A. Voronkov, MIT Press, Cambridge, Mass., 2001.","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] Birget, J.-C., \u201cState-complexity of finite-state devices, state compressibility and incompressibility,\u201d <i>Mathematical Systems Theory<\/i>, vol. 26 (1993), pp. 237\u201369.","DOI":"10.1007\/BF01371727"},{"key":"16","doi-asserted-by":"crossref","unstructured":"[16] Blackburn, P., J. van Benthem, and F. Wolter, <i>Handbook of Modal Logic<\/i>, Elsevier, 2006.","DOI":"10.1002\/9780470996751.ch27"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] Chandra, A. K., D. C. Kozen, and L. J. Stockmeyer, \u201cAlternation,\u201d <i>Journal of the ACM<\/i>, vol. 28 (1981), pp. 114\u201333.","DOI":"10.1145\/322234.322243"},{"key":"18","doi-asserted-by":"publisher","unstructured":"[18] Dijkstra, E. W., \u201cA note on two problems in connexion with graphs,\u201d <i>Numerische Mathematik<\/i>, vol. 1 (1959), pp. 269\u201371.","DOI":"10.1007\/BF01386390"},{"key":"19","unstructured":"[19] Garey, M. R., and D. S. Johnson, <i>Computers and Intractability: A Guide to the Theory of NP-Completeness<\/i>, Freeman, San Francisco, Calif., 1979."},{"key":"20","doi-asserted-by":"publisher","unstructured":"[20] Horrocks, I., U. Sattler, and S. Tobies, \u201cPractical reasoning for very expressive description logics,\u201d <i>Logic Journal of the IGPL<\/i>, vol. 8 (2000), pp. 239\u201364.","DOI":"10.1093\/jigpal\/8.3.239"},{"key":"21","doi-asserted-by":"publisher","unstructured":"[21] Jiang, T., and B. Ravikumar, \u201cA note on the space complexity of some decision problems for finite automata,\u201d <i>Information Processing Letters<\/i>, vol. 40 (1991), pp. 25\u201331.","DOI":"10.1016\/S0020-0190(05)80006-7"},{"key":"22","doi-asserted-by":"publisher","unstructured":"[22] Kozen, D., \u201cLower bounds for natural proof systems,\u201d pp. 254\u201366 in <i>18th Annual Symposium on Foundations of Computer Science (Providence, R.I., 1977)<\/i>, IEEE Computer Science, Long Beach, Calif., 1977.","DOI":"10.1109\/SFCS.1977.16"},{"key":"23","doi-asserted-by":"publisher","unstructured":"[23] Nieuwenhuis, R., A. Oliveras, and C. Tinelli, \u201cSolving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL (<i>T<\/i>),\u201d <i>Journal of the ACM<\/i>, vol. 53 (2006), pp. 937\u201377.","DOI":"10.1145\/1217856.1217859"},{"key":"24","doi-asserted-by":"publisher","unstructured":"[24] Savitch, W. J., \u201cRelationships between nondeterministic and deterministic tape complexities,\u201d <i>Journal of Computer and System Sciences<\/i>, vol. 4 (1970), pp. 177\u201392.","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"25","unstructured":"[25] Schild, K., \u201cA correspondence theory for terminological logics: Preliminary report,\u201d pp. 466\u201371 in <i>Proceedings of the 12th International Joint Conference on Artificial Intelligence<\/i> (<i>IJCAI\u201991<\/i>), Kaufmann, San Francisco, Calif., 1991."},{"key":"26","unstructured":"[26] Sofronie-Stokkermans, V., \u201cLocality and subsumption testing in $\\mathcal{EL}$ and some of its extensions,\u201d pp. 315\u201339 in <i>Advances in Modal Logic, vol. 7<\/i>, edited by C. Areces and R. Goldblatt, College Publications, London, 2008."},{"key":"27","doi-asserted-by":"crossref","unstructured":"[27] Suntisrivaraporn, B., F. Baader, S. Schulz, and K. Spackman, \u201cReplacing SEP-triplets in SNOMED CT using tractable description logic operators,\u201d pp. 287\u201391 in <i>Proceedings of the 11th Conference on Artificial Intelligence in Medicine<\/i> (<i>AIME\u201907<\/i>), edited by R. Bellazzi, A. Abu-Hanna, and J. Hunter, vol. 4594 of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 2007.","DOI":"10.1007\/978-3-540-73599-1_38"},{"key":"28","doi-asserted-by":"publisher","unstructured":"[28] Wolter, F., and M. Zakharyaschev, \u201cUndecidability of the unification and admissibility problems for modal and description logics,\u201d <i>ACM Transactions on Computational Logic<\/i>, vol. 9 (2008), no. 25.","DOI":"10.1145\/1380572.1380574"}],"container-title":["Notre Dame Journal of Formal Logic"],"original-title":[],"link":[{"URL":"https:\/\/projecteuclid.org\/journalArticle\/Download?urlid=10.1215\/00294527-3555507","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,10,9]],"date-time":"2026-10-09T15:54:14Z","timestamp":1791561254000},"score":1,"resource":{"primary":{"URL":"https:\/\/projecteuclid.org\/journals\/notre-dame-journal-of-formal-logic\/volume-57\/issue-4\/Deciding-Unifiability-and-Computing-Local-Unifiers-in-the-Description-Logic\/10.1215\/00294527-3555507.full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,1]]},"references-count":28,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2016,1,1]]}},"URL":"https:\/\/doi.org\/10.1215\/00294527-3555507","relation":{},"ISSN":["0029-4527","1939-0726"],"issn-type":[{"value":"0029-4527","type":"print"},{"value":"1939-0726","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1,1]]}}}