Abstract
The Description Logic (DL) \({\mathcal {F\!L}_0}\) uses universal quantification, whereas its well-known counter-part \(\mathcal {E\!L}\) uses the existential one. While for \(\mathcal {E\!L}\) deciding subsumption in the presence of general TBoxes is tractable, this is no the case for \({\mathcal {F\!L}_0}\). We present a novel algorithm for solving the ExpTime-hard subsumption problem in \({\mathcal {F\!L}_0}\) w.r.t. general TBoxes, which is based on the computation of so-called least functional models. To build a such a model our algorithm treats TBox axioms as rules that are applied to objects of the interpretation domain. This algorithm is implemented in the \(\mathcal {F\!L}_{o}{} \textit{wer}\) reasoner, which uses a variant of the Rete pattern matching algorithm to find applicable rules. We present an evaluation of \(\mathcal {F\!L}_{o}{} \textit{wer}\) on a large set of TBoxes generated from real world ontologies. The experimental results indicate that our prototype implementation of the specialised technique for \({\mathcal {F\!L}_0}\) leads in most cases to a huge performance gain in comparison to the highly-optimised tableau reasoners.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Baader, F., Brandt, S., Lutz, C.: Pushing the \(\cal{EL}\) envelope. In: IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, 2005, pp. 364–369. http://ijcai.org/Proceedings/05/Papers/0372.pdf
Baader, F., Fernández Gil, O., Pensel, M.: Standard and Non-Standard Inferences in the Description Logic \(\cal{FL}_0\) using Tree Automata. LTCS-Report 18–04, Chair for Automata Theory, Institute for Theoretical Computer Science, TU Dresden, Dresden, Germany (2018). http://lat.inf.tu-dresden.de/research/reports.html
Baader, F., Fernández Gil, O., Marantidis, P.: Matching in the description logic \(\cal{FL}_0\) with respect to general TBoxes. In: LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2018, EPiC Series in Computing, EasyChair, vol. 57, pp. 76–94 (2018). http://www.easychair.org/publications/paper/XrXz
Baader, F., Fernández Gil, O., Pensel, M.: Standard and non-standard inferences in the description logic \(\cal{FL}_0\) using tree automata. In: GCAI-2018, 4th Global Conference on Artificial Intelligence, 2018, EPiC Series in Computing, EasyChair, vol. 55, pp. 1–14 (2018). http://www.easychair.org/publications/paper/H6d9
Baader, F., Marantidis, P., Okhotin, A.: Approximate unification in the description logic \(\cal{FL}_0\). In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS (LNAI), vol. 10021, pp. 49–63. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48758-8_4
Baader, F., Marantidis, P., Pensel, M.: The data complexity of answering instance queries in \(\cal{FL}_0\). In: Companion of the The Web Conference 2018, WWW 2018, ACM, pp. 1603–1607 (2018). https://doi.org/10.1145/3184558.3191618
Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Studia Logica 69(1), 5–40 (2001). https://doi.org/10.1023/A:1013882326814
Brachman, R.J., Levesque, H.J.: The tractability of subsumption in frame-based description languages. In: Proceedings of the National Conference on Artificial Intelligence, 1984, AAAI Press, pp. 34–37 (1984). http://www.aaai.org/Library/AAAI/1984/aaai84-036.php
Forgy, C.: Rete: a fast algorithm for the many patterns/many objects match problem. Artif. Intell. 19(1), 17–37 (1982). https://doi.org/10.1016/0004-3702(82)90020-0
Cuenca Grau, B., Horrocks, I., Motik, B., Parsia, B., Patel-Schneider, P.F., Sattler, U.: OWL 2: the next step for OWL. J. Web Semant. 6(4), 309–322 (2008)
Horridge, M., Bechhofer, S.: The OWL API: a java API for OWL ontologies. Seman. Web 2(1), 11–21 (2011)
Kazakov, Y., de Nivelle, H.: Subsumption of concepts in \(\cal{FL}_0\) for (cyclic) terminologies with respect to descriptive semantics is PSPACE-complete. In: Proceedings of the 2003 International Workshop on Description Logics (DL 2003), 2003, CEUR Workshop Proceedings. http://ceur-ws.org/Vol-81/kazakov.pdf
Krötzsch, M., Rudolph, S., Hitzler, P.: Complexity boundaries for Horn description logics. In: Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, AAAI Press, pp. 452–457 (2007). http://www.aaai.org/Library/AAAI/2007/aaai07-071.php
Michel, F.: Entwurf und Implementierung eines Systems zur Entscheidung von Subsumption in der Beschreibungslogik \(\cal{FL}_0\). Bachelor’s thesis, TU Dresden (2017). (in German)
Nebel, B.: Terminological reasoning is inherently intractable. Artif. Intell. 43(2), 235–249 (1990). https://doi.org/10.1016/0004-3702(90)90087-G
Parsia, B., Matentzoglu, N., Gonçalves, R.S., Glimm, B., Steigmiller, A.: The OWL reasoner evaluation (ORE) 2015 competition report. J. Autom. Reason. 59(4), 455–482 (2017)
Armas Romero, A., Cuenca Grau, B., Horrocks, I.: MORe: modular combination of OWL reasoners for ontology classification. In: Cudré-Mauroux, P., et al. (eds.) ISWC 2012. LNCS, vol. 7649, pp. 1–16. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35176-1_1
Simancik, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond Horn ontologies. In: IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, 2011, IJCAI/AAAI, pp. 1093–1098 (2011). https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-187
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Michel, F., Turhan, AY., Zarrieß, B. (2019). Efficient TBox Reasoning with Value Restrictions—Introducing the \(\mathcal {F\!L}_{o}{} \textit{wer}\) Reasoner. In: Fodor, P., Montali, M., Calvanese, D., Roman, D. (eds) Rules and Reasoning. RuleML+RR 2019. Lecture Notes in Computer Science(), vol 11784. Springer, Cham. https://doi.org/10.1007/978-3-030-31095-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-31095-0_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-31094-3
Online ISBN: 978-3-030-31095-0
eBook Packages: Computer ScienceComputer Science (R0)