{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:58:10Z","timestamp":1762102690448,"version":"3.40.5"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2022,3]]},"abstract":"Abstract<\/jats:title>The inexpressive Description Logic (DL) \n${\\cal F}{{\\cal L}_0}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, which has conjunction and value restriction as its only concept constructors, had fallen into disrepute when it turned out that reasoning in \n${\\cal F}{{\\cal L}_0}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> w.r.t. general TBoxes is Exp<\/jats:sc>Time<\/jats:sc>-complete, that is, as hard as in the considerably more expressive logic \n${\\cal A}{\\cal L}{\\cal C}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. In this paper, we rehabilitate \n${\\cal F}{{\\cal L}_0}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> by presenting a dedicated subsumption algorithm for \n${\\cal F}{{\\cal L}_0}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, which is much simpler than the tableau-based algorithms employed by highly optimized DL reasoners. Our experiments show that the performance of our novel algorithm, as prototypically implemented in our \n${\\cal F}{{\\cal L}_0}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>wer<\/jats:italic> reasoner, compares very well with that of the highly optimized reasoners. \n${\\cal F}{{\\cal L}_0}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>wer<\/jats:italic> can also deal with ontologies written in the extension \n${\\cal F}{{\\cal L}_ \\bot }$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> of \n${\\cal F}{{\\cal L}_0}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> with the top and the bottom concept by employing a polynomial-time reduction, shown in this paper, which eliminates top and bottom. We also investigate the complexity of reasoning in DLs related to the Horn-fragments of \n${\\cal F}{{\\cal L}_0}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> and \n${\\cal F}{{\\cal L}_ \\bot }$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1017\/s1471068421000466","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T16:08:10Z","timestamp":1634314090000},"page":"162-192","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Efficient TBox Reasoning with Value Restrictions using the wer<\/i> Reasoner"],"prefix":"10.1017","volume":"22","author":[{"given":"FRANZ","family":"BAADER","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5999-2583","authenticated-orcid":false,"given":"PATRICK","family":"KOOPMANN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"FRIEDRICH","family":"MICHEL","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6336-335X","authenticated-orcid":false,"given":"ANNI-YASMIN","family":"TURHAN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"BENJAMIN","family":"ZARRIESS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"S1471068421000466_ref2","unstructured":"Baader, F. , Brandt, S. and Lutz, C. 2005. Pushing the ${\\cal E}{\\cal L}$ envelope. In Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJCAI 2005), Kaelbling, L. P. and Saffiotti, A. , Eds. Edinburgh, UK. Morgan Kaufmann, Los Altos, 364\u2013369."},{"key":"S1471068421000466_ref11","doi-asserted-by":"crossref","unstructured":"Brachman, R. J. , McGuinness, D. L. , Patel-Schneider, P. F. , Alperin Resnick, L. and Borgida, A. 1991. Living with CLASSIC: When and how to use a KL-ONE-like language. In Principles of Semantic Networks, Sowa, J. F. , Eds. Morgan Kaufmann, Los Altos, 401\u2013456.","DOI":"10.1016\/B978-1-4832-0771-1.50022-9"},{"key":"S1471068421000466_ref30","doi-asserted-by":"crossref","unstructured":"Romero, A. A. , Cuenca Grau, B. and Horrocks, I. 2012. More: Modular combination of OWL reasoners for ontology classification. In International Semantic Web Conference (1), vol. 7649 of Lecture Notes in Computer Science. Springer, 1\u201316.","DOI":"10.1007\/978-3-642-35176-1_1"},{"key":"S1471068421000466_ref22","unstructured":"Kr\u00f6tzsch, M. , Rudolph, S. and Hitzler, P. 2007. Complexity boundaries for Horn description logics. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, July 22\u201326, 2007, Vancouver, British Columbia, Canada. AAAI Press, 452\u2013457."},{"year":"2019","author":"Michel","key":"S1471068421000466_ref26"},{"key":"S1471068421000466_ref9","doi-asserted-by":"publisher","DOI":"10.1023\/A:1013882326814"},{"key":"S1471068421000466_ref31","unstructured":"Schild, K. 1991. A correspondence theory for terminological logics: Preliminary report. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI\u201991), 466\u2013471."},{"key":"S1471068421000466_ref12","doi-asserted-by":"publisher","DOI":"10.1207\/s15516709cog0902_1"},{"key":"S1471068421000466_ref1","unstructured":"Baader, F. 1990. Terminological cycles in KL-ONE-based knowledge representation languages. In Proc. of the 8th Nat. Conf. on Artificial Intelligence (AAAI\u201990), Boston, MA, USA, 621\u2013626."},{"key":"S1471068421000466_ref16","doi-asserted-by":"publisher","DOI":"10.1093\/bib\/bbv011"},{"key":"S1471068421000466_ref24","unstructured":"Matentzoglu, N. , Bail, S. and Parsia, B. 2013. A snapshot of the OWL Web. In The Semantic Web - ISWC 2013 - 12th International Semantic Web Conference, Sydney, NSW, Australia, October 21\u201325, 2013, Proceedings, Part I, Alani, H. , Kagal, L. , Fokoue, A. , Groth, P. T. , Biemann, C. , Parreira, J. X. , Aroyo, L. , Noy, N. F. , Welty, C. and Janowicz, K. , Eds. vol. 8218 of Lecture Notes in Computer Science. Springer, 331\u2013346."},{"key":"S1471068421000466_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/122296.122314"},{"key":"S1471068421000466_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.websem.2003.07.001"},{"key":"S1471068421000466_ref21","unstructured":"Kazakov, Y. and de Nivelle, H. 2003. Subsumption of concepts in ${\\cal F}{{\\cal L}_0}$ for (cyclic) terminologies with respect to descriptive semantics is PSPACE-complete. In Proc. of the 2003 Description Logic Workshop (DL 2003). CEUR Electronic Workshop Proceedings, http:\/\/CEUR-WS.org\/Vol-81\/."},{"key":"S1471068421000466_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(82)90020-0"},{"key":"S1471068421000466_ref5","unstructured":"Baader, F. , Fernandez Gil, O. and Pensel, M. 2018a. Standard and non-standard inferences in the description logic ${\\cal F}{{\\cal L}_0}$ using tree automata. In GCAI-2018, 4th Global Conference on Artificial Intelligence, Lee, D. D. , Steen, A. and Walsh, T. , Eds. vol. 55 of EPiC Series in Computing. EasyChair, 1\u201314."},{"key":"S1471068421000466_ref18","doi-asserted-by":"publisher","DOI":"10.3233\/SW-2011-0025"},{"key":"S1471068421000466_ref32","unstructured":"Siman\u010d\u00edk, F. , Kazakov, Y. and Horrocks, I. 2011. Consequence-based reasoning beyond Horn ontologies. In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Walsh, T. , Ed. IJCAI\/AAAI, 1093\u20131098."},{"volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","year":"2003","author":"Baader","key":"S1471068421000466_ref3"},{"key":"S1471068421000466_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/9781139025355"},{"key":"S1471068421000466_ref13","unstructured":"Brandt, S. 2004. Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and\u2014what else? In Proc. of the 16th Eur. Conf. on Artificial Intelligence (ECAI 2004), de M\u00e1ntaras, R. L. and Saitta, L. , Eds., pp. 298\u2013302."},{"key":"S1471068421000466_ref4","unstructured":"Baader, F. , Fernandez Gil, O. and Marantidis, P. 2018. Matching in the description logic ${\\cal F}{{\\cal L}_0}$ with respect to general TBoxes. In LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Barthe, G. , Sutcliffe, G. and Veanes, M. , Eds. vol. 57 of EPiC Series in Computing. EasyChair, 76\u201394."},{"key":"S1471068421000466_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.websem.2008.05.001"},{"key":"S1471068421000466_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2422085.2422087"},{"key":"S1471068421000466_ref7","doi-asserted-by":"crossref","unstructured":"Baader, F. , Marantidis, P. and Okhotin, A. 2016. Approximate unification in the description logic ${\\cal F}{{\\cal L}_0}$ . In Logics in Artificial Intelligence - 15th European Conference, JELIA 2016, Proceedings, Michael, L. and Kakas, A. C. , Eds. vol. 10021 of Lecture Notes in Computer Science, 49\u201363.","DOI":"10.1007\/978-3-319-48758-8_4"},{"key":"S1471068421000466_ref17","unstructured":"Hofmann, M. 2005. Proof-theoretic approach to description-logic. In Proc. of the 20th IEEE Symp. on Logic in Computer Science (LICS 2005), Panangaden, P. , Ed. IEEE Computer Society Press, 229\u2013237."},{"key":"S1471068421000466_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/122296.122310"},{"key":"S1471068421000466_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(90)90087-G"},{"key":"S1471068421000466_ref20","unstructured":"Kazakov, Y. 2009. Consequence-driven reasoning for Horn ${\\cal S}{\\cal H}{\\cal I}{\\cal Q}$ ontologies. In Proc. of the 21st Int. Joint Conf. on Artificial Intelligence (IJCAI 2009), C. Boutilier, Ed. IJCAI\/AAAI, 2040\u20132045."},{"key":"S1471068421000466_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s13218-020-00651-0"},{"key":"S1471068421000466_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9406-8"},{"key":"S1471068421000466_ref8","doi-asserted-by":"crossref","unstructured":"Baader, F. , Marantidis, P. and Pensel, M. 2018b. The data complexity of answering instance queries in ${\\cal F}{{\\cal L}_0}$ . In Companion of the The Web Conference WWW, Champin, P. , Gandon, F. L. , Lalmas, M. and Ipeirotis, P. G. , Eds. ACM, 1603\u20131607.","DOI":"10.1145\/3184558.3191618"},{"key":"S1471068421000466_ref33","doi-asserted-by":"crossref","unstructured":"Woods, W. A. and Schmolze, J. G. 1992. The KL-ONE family. In Semantic Networks in Artificial Intelligence, F. W. Lehmann, Ed., pp. 133\u2013178. Pergamon Press. Published as a special issue of Computers & Mathematics with Applications 23, 2\u20139.","DOI":"10.1016\/0898-1221(92)90139-9"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068421000466","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T04:15:36Z","timestamp":1649045736000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068421000466\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,3]]}},"alternative-id":["S1471068421000466"],"URL":"https:\/\/doi.org\/10.1017\/s1471068421000466","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}