A sequent calculus for reasoning in four-valued Description Logics

Description Logics (DLs, for short) provide a logical reconstruction of the so-called frame-based knowledge representation languages. Originally, four-valued DLs have been proposed in order to develop expressively powerful DLs with tractable subsumption algorithms. Recently, four-valued DLs have been proposed as a model for (multimedia) document retrieval. In this context, the main reasoning task is instance checking. Unfortunately, the known subsumption algorithms for four-valued DLs, based on "structural" subsumption, do not work with respect to the semantics proposed in the DL-based approach to document retrieval. Moreover, they are unsuitable for solving the instance checking problem, as this latter problem is more general than the subsumption problem. We present an alternative decision procedure for four-valued DLs with the aim to solve these problems. The decision procedure is a sequent calculus for instance checking. Since in general the four-valued subsumption problem can be reduced to the four-valued instance checking problem, we obtain a decision procedure for the subsumption problem. Some related complexity results will be presented.