{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T02:40:01Z","timestamp":1749004801712,"version":"3.41.0"},"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]]},"DOI":"10.1215\/00294527-3555507","type":"journal-article","created":{"date-parts":[[2016,7,19]],"date-time":"2016-07-19T18:17:05Z","timestamp":1468952225000},"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":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nguyen Thanh","family":"Binh","sequence":"additional","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":"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":[[2025,6,4]],"date-time":"2025-06-04T02:15:35Z","timestamp":1749003335000},"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"],"issn-type":[{"type":"print","value":"0029-4527"}],"subject":[],"published":{"date-parts":[[2016,1,1]]}}}