Philippe Balbiani

Solving equations in modal and description logics, 18th International Conference on Principles of Knowledge Representation and Reasoning, online event, November 2021.
- Personal details of the presenter: Philippe Balbiani is CNRS Researcher (directeur de recherche) at the Institut de recherche en informatique de Toulouse (Toulouse, France). His research concerns the theory of non-classical logics, their mechanization and the algorithmic aspects of qualitative reasoning about space and time.
- Abstract of the tutorial: Originally motivated by automatic deduction tools, as described in Babenyshev et al. (2010), the unification problem in modal logics constitutes today the heart of an active research area in which, nevertheless, much remains to be done. Within the context of description logics, the main motivation for investigating the unification problem, as described in Baader and Narendran (2001), was to propose new reasoning services in the maintenance of knowledge bases like, for example, the elimination of redundancies in the descriptions of concepts. In this tutorial, we will give a survey of the results on unification in these non-classical logics and we will present some of the open problems whose solution will have a great impact on the future of the area.
- Potential target audience: This tutorial will emphasize important concepts in unification in non-classical logics such as modal logics and description logics and illustrate them by working through accessible examples. It is intended for researchers and students interested in gaining broad coverage of modal logics and description logics and engineers considering developing logic-based applications.
- Prerequisites: There are no special prerequisites for the tutorial. We will assume basic knowledge of Classical Propositional Logic. Familiarity with basic concepts and approaches to modal logics and description logics will be helpful. In any case, the tutorial will be completely self-contained. It will not deal with low level programming or implementation and does not presume any knowledge of a particular programming language.
- Description of the tutorial: Within the context of modal logics, given formula F, automated deduction systems allow their users to determine whether F is satisfiable. However, checking satisfiability of formulas is not always sufficient and it has appeared, considering applications of modal logics in Computer Science and Artificial Intelligence, that new inference capabilities are required. One of them is the unification of formulas. The problem whether there exists a decision procedure for determining whether a given modal formula is unifiable has been proved to be decidable in modal logic S4 by Rybakov (1984). See also Ghilardi (2000). Within the context of description logics, given concept terms C,D, automated deduction systems allow their users to determine whether C is subsumed by D. However, checking subsumption of concepts is not always sufficient and it has appeared, considering applications in the maintenance of knowledge bases, that new inference capabilities are required. One of them is the unification of concept terms. It has been introduced by Baader and Narendran (2001) as a tool for detecting redundancies in knowledge bases. See also Baader and Kusters (2000, 2001, 2006), Baader et al. (2012) and Baader and Morawska (2009, 2010). Today, the unification problem in non-classical logics such as modal logics and description logics constitute the heart of an active area of research. See Baader and Ghilardi (2011). Nevertheless, much remains to be done, seeing that little is known about these problems in some of the most well-known non-classical logics considered in Computer Science and Artificial Intelligence. For example, the decidability of the unification problem for the following non-classical logics remains open: description logic ALC, multi-agent epistemic logics, sub-Boolean modal logics.
- Outline of the tutorial: In this tutorial, we will give a survey of the results on unification in these non-classical logics and we will present some of the open problems whose solution will have a great impact on the future of the area. We will assume very basic knowledge of fundamental concepts and standard facts of modal logics and description logics, but everything will be self-contained. A tentative outline can be the following:
  - Introductory part about unification in equational theories (decidability and complexity, computation of a minimal complete set of unifiers, unification types, applications, etc); case of Boolean unification; introductory part motivating the consideration of unification in modal logics and description logics.
  - Unification and matching in description logics (decidability and complexity, computation of a minimal complete set of unifiers, unification types, applications, etc); unification in specific description logics such as EL, FL0, etc.
  - Unification in multimodal, tense and epistemic logics considered in Computer Science and Artificial Intelligence (S5, KD45, tense logics with linear or branching time, epistemic logics with common knowledge, logics with the universal modality, etc).
Unification in Description Logics and Modal Logics, European Summer School in Logic, Language and Information, Heinrich Heine University of Düsseldorf (Düsseldorf, Germany), 8 hours, August 2013, in collaboration with Cigdem Gencer.
Spatial Logics, European Summer School in Logic, Language and Information, Heinrich Heine University of Düsseldorf (Düsseldorf, Germany), 8 hours, August 2013.
Region-Based Theories of Space, German Conference on Artificial Intelligence - KI 2012 (Saarbrücken, Germany), 6 hours, September 2012.
Region-Based Theories of Space, European Summer School in Logic, Language and Information, Ljubljana University (Ljubljana, Slovenia), 8 hours, August 2011.
Formal Concept Analysis : Foundations and Applications, Computer Science Summer School, Notre-Dame University (Zouk Mosbeh, Lebanon), 6 hours, July 2011.