A Sequent Calculus for Reasoning in Four-Valued Description
Logics.
In Proc. of the Int. Conf. on Analytic Tableaux and
Related Methods (TABLEAUX-97), Pont-a-Mousson, France, 1997.
Abstract:
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.