Unification in Description Logics
Advanced Course at the 31st European Summer School in Logic, Language and Information (ESSLLI 2019)
Lecturer: Dr. Oliver Fernández Gil (Chair of Automata Theory, TU Dresden)
The general content of this course is based on the following survey (additional reading materials are provided for each specific topic):
Baader, F., Ghilardi, S. Unification in Modal and Description Logics. Logic Journal of the IGPL 19(6), 705-730 (2011).
Course programme (... to be updated)
Part I: Introduction (slides)
- What is unification?
- Siekmann, J.H. Unification Theory. J. Symb. Comput. 7(3/4): 207-274 (1989).
- Baader, F., Snyder, W. Unification Theory. In J. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, vol. I, pp. 447-533. Elsevier Science Publishers, 2001.
- A brief overview of Description Logics.
- Baader, F., Calvanese, D., McGuinness, D., Nardi, D. and Patel-Schneider, P.F., editors: The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003.
- Baader, F., Horrocks, I., Lutz, C., Sattler, U. An Introduction to Description Logics. Cambridge University Press, 2017.
- Unification in Description Logics: motivation and formal definitions.
Part II: Unification in the Description Logic EL (slides)
- Decidability, Complexity, Computing minimal EL-unifiers.
- Baader, F., Küsters, R. Matching in Description Logics with Existential Restrictions. In: Proc of the 7th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2000), pp. 261-272, 2000.
- Baader, F., Morawska, B.: Unification in the Description Logic EL. Logical Methods in Computer Science, 6(3), 2010.
- Baader, F., Morawska, B.: SAT Encoding of Unification in EL. In: Proc. of the 17th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2010). LNCS, vol. 6397, pp. 97-111. Springer-Verlag, 2010.
- Baader, F., Borgwardt, S., Morawska, B. Computing minimal EL-unifiers is hard. In: Proc. of the 9th Conference in Advances in Modal Logics (AiML 2012), pp 18-35. College Publications, 2012.
- Unification modulo EL-TBoxes
- Baader, F., Borgwardt, S., Morawska, B. Extending Unification in EL towards General TBoxes. In: Proc of the 13th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2012), pp. 568-572. AAAI Press/The MIT Press, 2012.
Part III: Unification in the Description Logic FL_0 (slides)
- Decidability and Complexity.
- Baader, F., Narendran, P. Unification of Concept Terms in Description Logics. Journal of Symbolic Computation, 31(3):227-305, 2001.
- Baader, F., Küsters, R. Unification in a Description Logic with transitive closure of roles. In: Proc. of the 8th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001). LNAI, vol. 2250, pp. 217-232. Springer-Verlag, 2001. Springer-Verlag.
- Matching with respect to general TBoxes.
- Baader, F., Fernández Gil, O., Marantidis, P. Matching in the Description Logic FL_0 w.r.t. general TBoxes. In: Proc. of the 8th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2018), vol. 57, pp. 76-94. EasyChair, 2018.
Part IV: Related research in Modal Logics (very brief) (slides)